English
Two pseudo-metric structures with the same distance function are equal.
Русский
Две псевдометрические структуры, имеющие одну и ту же функцию расстояния, совпадают.
LaTeX
$$$m.toDist = m'.toDist \Rightarrow m = m'$$$
Lean4
/-- Two pseudo metric space structures with the same distance function coincide. -/
@[ext]
theorem ext {α : Type*} {m m' : PseudoMetricSpace α} (h : m.toDist = m'.toDist) : m = m' :=
by
let d := m.toDist
obtain ⟨_, _, _, _, hed, _, hU, _, hB⟩ := m
let d' := m'.toDist
obtain ⟨_, _, _, _, hed', _, hU', _, hB'⟩ := m'
obtain rfl : d = d' := h
congr
· ext x y : 2
rw [hed, hed']
· exact UniformSpace.ext (hU.trans hU'.symm)
· ext : 2
rw [← Filter.mem_sets, ← Filter.mem_sets, hB, hB']
