ext — Mathlib

English

Two pseudo-emetric spaces with same edist are equal; extensionality principle.

Русский

У двух псевдо-эмитрических пространств с одинаковым edist совпадают все структуры.

LaTeX

$$$ ed = ed' \Rightarrow m = m' $$$

Lean4

/-- Two pseudo emetric space structures with the same edistance function coincide. -/
@[ext]
protected theorem ext {α : Type*} {m m' : PseudoEMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m' :=
  by
  obtain ⟨_, _, _, U, hU⟩ := m; rename EDist α => ed
  obtain ⟨_, _, _, U', hU'⟩ := m'; rename EDist α => ed'
  congr 1
  exact UniformSpace.ext (((show ed = ed' from h) ▸ hU).trans hU'.symm)

Похожие утверждения