nndist_toLp_snd — Mathlib

English

The distance between the second-coordinate embeddings is preserved: nndist(toLp p (0,y1), toLp p (0,y2)) = nndist(y1,y2).

Русский

Расстояние между вторыми компонентами сохраняется: nndist(toLp p (0,y1), toLp p (0,y2)) = nndist(y1,y2).

LaTeX

$$$\mathrm{nndist}\bigl(toLp(p)(0,y_1), toLp(p)(0,y_2)\bigr) = \mathrm{nndist}(y_1,y_2).$$$

Lean4

@[simp]
theorem nndist_toLp_snd (y₁ y₂ : β) : nndist (toLp p ((0 : α), y₁)) (toLp p (0, y₂)) = nndist y₁ y₂ := by
  rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, Prod.mk_sub_mk, sub_zero, nnnorm_toLp_inr]

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