α : Type u
β : Type v
X : Type ?u.281110
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
⊢ SeparableSpace α
α : Type u
β : Type v
X : Type ?u.281110
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
⊢ SecondCountableTopology α
suffices SeparableSpace α by exact UniformSpace.secondCountable_of_separable α
α : Type u
β : Type v
X : Type ?u.281110
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure (T n)
⊢ SeparableSpace α
α : Type u
β : Type v
X : Type ?u.281110
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
⊢ SeparableSpace α
choose T _ hTc hsubT using fun n =>
  subset_countable_closure_of_compact (isCompact_compactCovering α n)
α : Type u
β : Type v
X : Type ?u.281110
inst✝¹ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure (T n)
x : α
⊢ x ∈ closure (⋃ (n : ℕ), T n)
α : Type u
β : Type v
X : Type ?u.281110
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure (T n)
⊢ SeparableSpace α
refine' ⟨⟨⋃ n, T n, countable_iUnion hTc, fun x => _⟩⟩
case intro
α : Type u
β : Type v
X : Type ?u.281110
inst✝¹ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure (T n)
x : α
n : ℕ
hn : x ∈ compactCovering α n
⊢ x ∈ closure (⋃ (n : ℕ), T n)
α : Type u
β : Type v
X : Type ?u.281110
inst✝¹ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure (T n)
x : α
⊢ x ∈ closure (⋃ (n : ℕ), T n)
rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering α) x with ⟨n, hn⟩
no goals
case intro
α : Type u
β : Type v
X : Type ?u.281110
inst✝¹ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure (T n)
x : α
n : ℕ
hn : x ∈ compactCovering α n
⊢ x ∈ closure (⋃ (n : ℕ), T n)
exact closure_mono (subset_iUnion _ n) (hsubT _ hn)
no goals
α : Type u
β : Type v
X : Type ?u.281110
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
this : SeparableSpace α
⊢ SecondCountableTopology α
exact UniformSpace.secondCountable_of_separable α