nndist_single_same — Mathlib

English

Similarly, the nonnegative distance between the i-th coordinate vectors with scalars a and b equals the nonnegative distance between a and b in 𝕜.

Русский

Аналогично, между векторами, имеющими в i-й координате a и b соответственно, нон-нормированное расстояние равно между a и b в 𝕜.

LaTeX

$$$\mathrm{nndist}(\mathrm{EuclideanSpace}.single(i, a), \mathrm{EuclideanSpace}.single(i, b)) = \mathrm{nndist}(a, b)$$$

Lean4

@[simp]
theorem nndist_single_same (i : ι) (a b : 𝕜) :
    nndist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = nndist a b :=
  PiLp.nndist_toLp_single_same 2 (fun _ => 𝕜) i a b

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