α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
⊢ x = y
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
⊢ x = y
have : SeparatedSpace (Completion α) := by infer_instance
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
⊢ (x, y) ∈ s
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
⊢ x = y
refine' separated_def.1 this x y fun s hs ↦ _
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ (x, y) ∈ s
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
⊢ (x, y) ∈ s
rcases (Completion.mem_uniformity_dist s).1 hs with ⟨ε, εpos, hε⟩
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
ε : ℝ
εpos : ε > dist x y
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ (x, y) ∈ s
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ (x, y) ∈ s
rw [← h] at εpos
no goals
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
ε : ℝ
εpos : ε > dist x y
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ (x, y) ∈ s
exact hε εpos
no goals
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
⊢ SeparatedSpace (Completion α)
infer_instance