α : Type u_2
β : Type u_1
γ : Type ?u.19398
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s
α : Type u_2
β : Type u_1
γ : Type ?u.19398
t : TopologicalSpace β
s : Set α
f : α → β
⊢ IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s
letI := t.induced f
α : Type u_2
β : Type u_1
γ : Type ?u.19398
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = sᶜ) ↔ ∃ t_1, IsOpen (t_1ᶜ) ∧ f ⁻¹' t_1 = s
α : Type u_2
β : Type u_1
γ : Type ?u.19398
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s
simp only [← isOpen_compl_iff, isOpen_induced_iff]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.19398
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = sᶜ) ↔ ∃ t_1, IsOpen (t_1ᶜ) ∧ f ⁻¹' t_1 = s
exact compl_surjective.exists.trans (by simp only [preimage_compl, compl_inj_iff])
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.19398
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ x, IsOpen (xᶜ) ∧ f ⁻¹' xᶜ = sᶜ) ↔ ∃ t_1, IsOpen (t_1ᶜ) ∧ f ⁻¹' t_1 = s
simp only [preimage_compl, compl_inj_iff]