case intro.intro
α : Type u
t : TopologicalSpace α
s u : Set α
hu : IsSeparable u
cs : Set α
cs_count : Set.Countable cs
hcs : s ⊆ closure cs
⊢ IsSeparable (s ∪ u)
α : Type u
t : TopologicalSpace α
s u : Set α
hs : IsSeparable s
hu : IsSeparable u
⊢ IsSeparable (s ∪ u)
rcases hs with ⟨cs, cs_count, hcs⟩
case intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s u cs : Set α
cs_count : Set.Countable cs
hcs : s ⊆ closure cs
cu : Set α
cu_count : Set.Countable cu
hcu : u ⊆ closure cu
⊢ IsSeparable (s ∪ u)
case intro.intro
α : Type u
t : TopologicalSpace α
s u : Set α
hu : IsSeparable u
cs : Set α
cs_count : Set.Countable cs
hcs : s ⊆ closure cs
⊢ IsSeparable (s ∪ u)
rcases hu with ⟨cu, cu_count, hcu⟩
case intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s u cs : Set α
cs_count : Set.Countable cs
hcs : s ⊆ closure cs
cu : Set α
cu_count : Set.Countable cu
hcu : u ⊆ closure cu
⊢ s ∪ u ⊆ closure (cs ∪ cu)
case intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s u cs : Set α
cs_count : Set.Countable cs
hcs : s ⊆ closure cs
cu : Set α
cu_count : Set.Countable cu
hcu : u ⊆ closure cu
⊢ IsSeparable (s ∪ u)
refine' ⟨cs ∪ cu, cs_count.union cu_count, _⟩
no goals
case intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s u cs : Set α
cs_count : Set.Countable cs
hcs : s ⊆ closure cs
cu : Set α
cu_count : Set.Countable cu
hcu : u ⊆ closure cu
⊢ s ∪ u ⊆ closure (cs ∪ cu)
exact
  union_subset (hcs.trans (closure_mono (subset_union_left _ _)))
    (hcu.trans (closure_mono (subset_union_right _ _)))