ext — Mathlib

English

Two metric space structures on the same set that share the same distance function are identical.

Русский

Две метрические структуры на одном множестве с одинаковой функцией расстояния coincide.

LaTeX

$$$m = m'$ whenever $m.{toDist}=m'.{toDist}$.$$

Lean4

/-- Two metric space structures with the same distance coincide. -/
@[ext]
theorem ext {α : Type*} {m m' : MetricSpace α} (h : m.toDist = m'.toDist) : m = m' := by cases m; cases m'; congr; ext1;
  assumption

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