dist_eq — Mathlib

English

The distance on X ⊕ Y is equal to the sum of the component distances under the glued metric; equivalently Sum.dist p q equals the glueDist with fixed basepoints.

Русский

Расстояние на X⊕Y равно сумме расстояний по компонентам под склеенной метрикой; эквивалентно Sum.dist p q равняется glueDist с фиксированными базовыми точками.

LaTeX

$$$ \mathrm{Sum}.\mathrm{dist} (p,q) = \mathrm{glueDist}(Φ,Ψ,1)(p,q). $$$

Lean4

theorem dist_eq {x y : X ⊕ Y} : dist x y = Sum.dist x y :=
  rfl

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