α : Type u_2
β : Type u_1
t✝ : TopologicalSpace β
f✝ : α → β
t : TopologicalSpace β
f : α → β
s : Set α
this : TopologicalSpace α := induced f t
⊢ IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
α : Type u_2
β : Type u_1
t✝ : TopologicalSpace β
f✝ : α → β
t : TopologicalSpace β
f : α → β
s : Set α
⊢ IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
letI := t.induced f
no goals
α : Type u_2
β : Type u_1
t✝ : TopologicalSpace β
f✝ : α → β
t : TopologicalSpace β
f : α → β
s : Set α
this : TopologicalSpace α := induced f t
⊢ IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
simp only [← closure_subset_iff_isClosed, subset_def, closure_induced]