dist_toLp_single_same — Mathlib

English

A single coordinate undergoes a linear isometric equivalence, leaving other coordinates fixed.

Русский

Одна координата изменяется при помощи линейной изометрии, прочие координаты остаются неизменными.

LaTeX

$$$\text{LinearIsometryEquiv.piLpCongrRightSingle}(p,e,i,v) = \text{toLp}(p, \Pi.single i (e_i v))$$$

Lean4

@[simp]
theorem dist_toLp_single_same (i : ι) (b₁ b₂ : β i) :
    dist (toLp p (Pi.single i b₁)) (toLp p (Pi.single i b₂)) = dist b₁ b₂ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| nndist_toLp_single_same p β i b₁ b₂

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