case intro.intro
α : Type u
t : TopologicalSpace α
s c : Set α
c_count : Set.Countable c
hs : s ⊆ _root_.closure c
⊢ IsSeparable (_root_.closure s)
α : Type u
t : TopologicalSpace α
s : Set α
hs : IsSeparable s
⊢ IsSeparable (_root_.closure s)
rcases hs with ⟨c, c_count, hs⟩
no goals
case intro.intro
α : Type u
t : TopologicalSpace α
s c : Set α
c_count : Set.Countable c
hs : s ⊆ _root_.closure c
⊢ IsSeparable (_root_.closure s)
exact ⟨c, c_count, by simpa using closure_mono hs⟩
no goals
α : Type u
t : TopologicalSpace α
s c : Set α
c_count : Set.Countable c
hs : s ⊆ _root_.closure c
⊢ _root_.closure s ⊆ _root_.closure c
simpa using closure_mono hs