case mp
α : Type u
t : TopologicalSpace α
⊢ IsSeparable univ → SeparableSpace α

case mpr
α : Type u
t : TopologicalSpace α
⊢ SeparableSpace α → IsSeparable univ
α : Type u
t : TopologicalSpace α
⊢ IsSeparable univ ↔ SeparableSpace α
constructor
case mp.intro.intro
α : Type u
t : TopologicalSpace α
c : Set α
c_count : Set.Countable c
hc : univ ⊆ closure c
⊢ SeparableSpace α
case mp
α : Type u
t : TopologicalSpace α
⊢ IsSeparable univ → SeparableSpace α
rintro ⟨c, c_count, hc⟩
no goals
case mp.intro.intro
α : Type u
t : TopologicalSpace α
c : Set α
c_count : Set.Countable c
hc : univ ⊆ closure c
⊢ SeparableSpace α
refine' ⟨⟨c, c_count, by rwa [dense_iff_closure_eq, ← univ_subset_iff]⟩⟩
no goals
α : Type u
t : TopologicalSpace α
c : Set α
c_count : Set.Countable c
hc : univ ⊆ closure c
⊢ Dense c
rwa [dense_iff_closure_eq, ← univ_subset_iff]
case mpr
α : Type u
t : TopologicalSpace α
h : SeparableSpace α
⊢ IsSeparable univ
case mpr
α : Type u
t : TopologicalSpace α
⊢ SeparableSpace α → IsSeparable univ
intro h
case mpr.intro.intro
α : Type u
t : TopologicalSpace α
h : SeparableSpace α
c : Set α
c_count : Set.Countable c
hc : Dense c
⊢ IsSeparable univ
case mpr
α : Type u
t : TopologicalSpace α
h : SeparableSpace α
⊢ IsSeparable univ
rcases exists_countable_dense α with ⟨c, c_count, hc⟩
no goals
case mpr.intro.intro
α : Type u
t : TopologicalSpace α
h : SeparableSpace α
c : Set α
c_count : Set.Countable c
hc : Dense c
⊢ IsSeparable univ
exact ⟨c, c_count, by rwa [univ_subset_iff, ← dense_iff_closure_eq]⟩
no goals
α : Type u
t : TopologicalSpace α
h : SeparableSpace α
c : Set α
c_count : Set.Countable c
hc : Dense c
⊢ univ ⊆ closure c
rwa [univ_subset_iff, ← dense_iff_closure_eq]