dist_up_up — Mathlib

English

Let α and β be pseudo-metric spaces. Replacing elements by their ULifted counterparts does not change distances: dist(ULift.up x, ULift.up y) = dist x y.

Русский

Пусть α и β — псевдометрические пространства. Преобразование элементов в их ULift-образ заменяет пары, не изменяя расстояния: dist(ULift.up x, ULift.up y) = dist x y.

LaTeX

$$$\operatorname{dist}(\mathrm{ULift.up}\,x, \mathrm{ULift.up}\,y) = \operatorname{dist}(x,y)$$$

Lean4

@[simp]
theorem dist_up_up (x y : β) : dist (ULift.up x) (ULift.up y) = dist x y :=
  rfl

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