edist_eq_of_L2 — Mathlib

English

For x,y ∈ PiLp 2 β, the edistance equals the Euclidean norm of the coordinatewise edistances: edist(x,y) = (∑ edist(x_i,y_i)^2)^{1/2}.

Русский

Для x,y в PiLp 2 β edist(x,y) задаётся как евклидова норма координатных edist: edist(x,y) = (∑ edist(x_i,y_i)^2)^{1/2}.

LaTeX

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

Lean4

theorem edist_eq_of_L2 (x y : PiLp 2 β) : edist x y = (∑ i, edist (x i) (y i) ^ 2) ^ (1 / 2 : ℝ) := by
  simp [PiLp.edist_eq_sum]

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