α : Type u_2
β : Type u_1
t✝ : TopologicalSpace β
f✝ : α → β
t : TopologicalSpace β
f : α → β
a : α
s : Set α
this : TopologicalSpace α := induced f t
⊢ a ∈ closure s ↔ f a ∈ closure (f '' s)
α : Type u_2
β : Type u_1
t✝ : TopologicalSpace β
f✝ : α → β
t : TopologicalSpace β
f : α → β
a : α
s : Set α
⊢ a ∈ closure s ↔ f a ∈ closure (f '' s)
letI := t.induced f
no goals
α : Type u_2
β : Type u_1
t✝ : TopologicalSpace β
f✝ : α → β
t : TopologicalSpace β
f : α → β
a : α
s : Set α
this : TopologicalSpace α := induced f t
⊢ a ∈ closure s ↔ f a ∈ closure (f '' s)
simp only [mem_closure_iff_frequently, nhds_induced, frequently_comap, mem_image, and_comm]