dist_eq — Mathlib

English

Let h be an isometric bijection between metric spaces α and β. Then for all x,y in α, dist(h(x), h(y)) = dist(x,y).

Русский

Пусть h — изометрическое взаимно однозначное отображение между метрическими пространствами α и β. Тогда для любых x,y ∈ α выполняется сохранение расстояния: dist(h(x), h(y)) = dist(x,y).

LaTeX

$$$\forall x,y \in \alpha:\ \operatorname{dist}(h(x),h(y)) = \operatorname{dist}(x,y)$$$

Lean4

protected theorem dist_eq {α β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] (h : α ≃ᵢ β) (x y : α) :
    dist (h x) (h y) = dist x y :=
  h.isometry.dist_eq x y

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