α✝ : Type u
β : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
⊢ ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
α✝ : Type u
β : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
⊢ SecondCountableTopology α
refine secondCountable_of_almost_dense_set fun ε ε0 => ?_
case intro.intro.intro
α✝ : Type u
β✝ : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_1
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
⊢ ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
α✝ : Type u
β : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
⊢ ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
rcases H ε ε0 with ⟨β, fβ, F, hF⟩
case intro.intro.intro
α✝ : Type u
β✝ : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_1
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
⊢ ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
case intro.intro.intro
α✝ : Type u
β✝ : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_1
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
⊢ ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
let Finv := rangeSplitting F
case intro.intro.intro
α✝ : Type u
β✝ : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_1
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
⊢ ∃ y, y ∈ range Finv ∧ dist x y ≤ ε
case intro.intro.intro
α✝ : Type u
β✝ : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_1
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
⊢ ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε
refine ⟨range Finv, ⟨countable_range _, fun x => ?_⟩⟩
case intro.intro.intro
α✝ : Type u
β✝ : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_1
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
x' : α := Finv { val := F x, property := (_ : F x ∈ range F) }
⊢ ∃ y, y ∈ range Finv ∧ dist x y ≤ ε
case intro.intro.intro
α✝ : Type u
β✝ : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_1
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
⊢ ∃ y, y ∈ range Finv ∧ dist x y ≤ ε
let x' := Finv ⟨F x, mem_range_self _⟩
case intro.intro.intro
α✝ : Type u
β✝ : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_1
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
x' : α := Finv { val := F x, property := (_ : F x ∈ range F) }
this : F x' = F x
⊢ ∃ y, y ∈ range Finv ∧ dist x y ≤ ε
case intro.intro.intro
α✝ : Type u
β✝ : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_1
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
x' : α := Finv { val := F x, property := (_ : F x ∈ range F) }
⊢ ∃ y, y ∈ range Finv ∧ dist x y ≤ ε
have : F x' = F x := apply_rangeSplitting F _
no goals
case intro.intro.intro
α✝ : Type u
β✝ : Type v
X : Type ?u.570966
ι : Type ?u.570969
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : MetricSpace α
H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_1
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
x' : α := Finv { val := F x, property := (_ : F x ∈ range F) }
this : F x' = F x
⊢ ∃ y, y ∈ range Finv ∧ dist x y ≤ ε
exact ⟨x', mem_range_self _, hF _ _ this.symm⟩