case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : Set.Countable c
hc : s ⊆ _root_.closure c
⊢ IsSeparable (f '' s)
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : IsSeparable s
f : α → β
hf : Continuous f
⊢ IsSeparable (f '' s)
rcases hs with ⟨c, c_count, hc⟩
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : Set.Countable c
hc : s ⊆ _root_.closure c
⊢ f '' s ⊆ _root_.closure (f '' c)
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : Set.Countable c
hc : s ⊆ _root_.closure c
⊢ IsSeparable (f '' s)
refine' ⟨f '' c, c_count.image _, _⟩
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : Set.Countable c
hc : s ⊆ _root_.closure c
⊢ s ⊆ f ⁻¹' _root_.closure (f '' c)
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : Set.Countable c
hc : s ⊆ _root_.closure c
⊢ f '' s ⊆ _root_.closure (f '' c)
rw [image_subset_iff]
no goals
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : Set.Countable c
hc : s ⊆ _root_.closure c
⊢ s ⊆ f ⁻¹' _root_.closure (f '' c)
exact hc.trans (closure_subset_preimage_closure_image hf)