nndist_toLp_fst — Mathlib

English

The distance between the first-coordinate embeddings is preserved: nndist(toLp p (x1,0), toLp p (x2,0)) = nndist(x1,x2).

Русский

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

LaTeX

$$$\mathrm{nndist}\bigl(toLp(p)(x_1,0),\; toLp(p)(x_2,0)\bigr) = \mathrm{nndist}(x_1,x_2).$$$

Lean4

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

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