α : Type u
β : Type v
X : Type ?u.281603
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), closedBall x ε) = univ
⊢ SeparableSpace α
α : Type u
β : Type v
X : Type ?u.281603
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), closedBall x ε) = univ
⊢ SecondCountableTopology α
suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α
case this
α : Type u
β : Type v
X : Type ?u.281603
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), closedBall x ε) = univ
⊢ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ univ ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε

α : Type u
β : Type v
X : Type ?u.281603
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), closedBall x ε) = univ
this : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ univ ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
⊢ SeparableSpace α
α : Type u
β : Type v
X : Type ?u.281603
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), closedBall x ε) = univ
⊢ SeparableSpace α
have : ∀ ε > 0, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε
case intro.intro.intro
α : Type u
β : Type v
X : Type ?u.281603
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), closedBall x ε) = univ
this : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ univ ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
t : Set α
htc : Set.Countable t
ht : univ ⊆ closure t
⊢ SeparableSpace α
α : Type u
β : Type v
X : Type ?u.281603
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), closedBall x ε) = univ
this : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ univ ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
⊢ SeparableSpace α
rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
X : Type ?u.281603
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), closedBall x ε) = univ
this : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ univ ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
t : Set α
htc : Set.Countable t
ht : univ ⊆ closure t
⊢ SeparableSpace α
exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩
no goals
case this
α : Type u
β : Type v
X : Type ?u.281603
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), closedBall x ε) = univ
⊢ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ univ ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
simpa only [univ_subset_iff] using hs