α : Type u
t : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), Set.Countable (c i)
h'c : ∀ (i : ι), s i ⊆ closure (c i)
⊢ IsSeparable (⋃ (i : ι), s i)
α : Type u
t : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable (⋃ (i : ι), s i)
choose c hc h'c using hs
α : Type u
t : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), Set.Countable (c i)
h'c : ∀ (i : ι), s i ⊆ closure (c i)
i : ι
⊢ s i ⊆ closure (⋃ (i : ι), c i)
α : Type u
t : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), Set.Countable (c i)
h'c : ∀ (i : ι), s i ⊆ closure (c i)
⊢ IsSeparable (⋃ (i : ι), s i)
refine' ⟨⋃ i, c i, countable_iUnion hc, iUnion_subset_iff.2 fun i => _⟩
no goals
α : Type u
t : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), Set.Countable (c i)
h'c : ∀ (i : ι), s i ⊆ closure (c i)
i : ι
⊢ s i ⊆ closure (⋃ (i : ι), c i)
exact (h'c i).trans (closure_mono (subset_iUnion _ i))