dist_sq_eq_of_L2 — Mathlib

English

For x,y ∈ PiLp 2 β, the squared distance equals the sum of squared coordinatewise distances: dist(x,y)^2 = ∑_i dist(x_i,y_i)^2.

Русский

Для x,y ∈ PiLp 2 β квадрат расстояния равен сумме квадратов координат: dist(x,y)^2 = ∑_i dist(x_i,y_i)^2.

LaTeX

$$$\operatorname{dist}(x,y)^{2} = \sum_{i\in ι} \operatorname{dist}(x_i,y_i)^{2},\quad x,y\in PiLp\;2\;β$$$

Lean4

theorem dist_sq_eq_of_L2 (x y : PiLp 2 β) : dist x y ^ 2 = ∑ i, dist (x i) (y i) ^ 2 := by
  simp_rw [dist_eq_norm, norm_sq_eq_of_L2, sub_apply]

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