nndist_eq — Mathlib

English

If h is an isometry between α and β, then for all x,y in α, nndist(h(x), h(y)) = nndist(x,y).

Русский

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

LaTeX

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

Lean4

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

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