α : Type u
β : Type v
X : Type ?u.439085
ι : Type ?u.439088
inst✝ : PseudoMetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), EMetric.closedBall x ε) = univ
α : Type u
β : Type v
X : Type ?u.439085
ι : Type ?u.439088
inst✝ : PseudoMetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
⊢ SecondCountableTopology α
refine' EMetric.secondCountable_of_almost_dense_set fun ε ε0 => _
case intro.intro
α : Type u
β : Type v
X : Type ?u.439085
ι : Type ?u.439088
inst✝ : PseudoMetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), EMetric.closedBall x ε) = univ
α : Type u
β : Type v
X : Type ?u.439085
ι : Type ?u.439088
inst✝ : PseudoMetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), EMetric.closedBall x ε) = univ
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 ε0 with ⟨ε', ε'0, ε'ε⟩
case intro.intro
α : Type u
β : Type v
X : Type ?u.439085
ι : Type ?u.439088
inst✝ : PseudoMetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : Set.Countable s
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
⊢ ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), EMetric.closedBall x ε) = univ
case intro.intro
α : Type u
β : Type v
X : Type ?u.439085
ι : Type ?u.439088
inst✝ : PseudoMetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), EMetric.closedBall x ε) = univ
choose s hsc y hys hyx using H ε' (by exact_mod_cast ε'0)
case intro.intro
α : Type u
β : Type v
X : Type ?u.439085
ι : Type ?u.439088
inst✝ : PseudoMetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : Set.Countable s
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
x : α
⊢ edist x (y x) ≤ ↑ε'
case intro.intro
α : Type u
β : Type v
X : Type ?u.439085
ι : Type ?u.439088
inst✝ : PseudoMetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : Set.Countable s
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
⊢ ∃ t, Set.Countable t ∧ (⋃ (x : α) (_ : x ∈ t), EMetric.closedBall x ε) = univ
refine' ⟨s, hsc, iUnion₂_eq_univ_iff.2 fun x => ⟨y x, hys _, le_trans _ ε'ε.le⟩⟩
no goals
case intro.intro
α : Type u
β : Type v
X : Type ?u.439085
ι : Type ?u.439088
inst✝ : PseudoMetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : Set.Countable s
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
x : α
⊢ edist x (y x) ≤ ↑ε'
exact_mod_cast hyx x
no goals
α : Type u
β : Type v
X : Type ?u.439085
ι : Type ?u.439088
inst✝ : PseudoMetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ ↑ε' > 0
exact_mod_cast ε'0