dist_single_same — Mathlib

English

For any i in ι and any scalars a, b in 𝕜, the distance between the vectors that differ only in the i-th coordinate equals the distance between a and b in 𝕜.

Русский

Для любого i∈ι и любых a, b∈𝕜 расстояние между векторами, отличающимися только в i-й координате, равно расстоянию между a и b в 𝕜.

LaTeX

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

Lean4

@[simp]
theorem dist_single_same (i : ι) (a b : 𝕜) :
    dist (EuclideanSpace.single i (a : 𝕜)) (EuclideanSpace.single i (b : 𝕜)) = dist a b :=
  PiLp.dist_toLp_single_same 2 (fun _ => 𝕜) i a b

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