edist_single_same — Mathlib

English

The edist between i-th coordinate vectors with scalars a and b is the same as the edist of a and b in 𝕜.

Русский

Расстояние по евклидовой метрике между i-й координатной векторой с a и b совпадает с расстоянием между a и b в 𝕜.

LaTeX

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

Lean4

@[simp]
theorem edist_single_same (i : ι) (a b : 𝕜) :
    edist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = edist a b :=
  PiLp.edist_toLp_single_same 2 (fun _ => 𝕜) i a b

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