nndist_toLp_single_same — Mathlib

English

The finitely-supported delta-like element is mapped to the corresponding coordinate, preserving the norm.

Русский

Элемент-распределение с одной единицей сохраняет норму при отображении в Lp.

LaTeX

$$$\|\text{piLpCongrLeftSingle}(p,e,i, v)\|_p = \|v\|$$$

Lean4

@[simp]
theorem nndist_toLp_single_same (i : ι) (b₁ b₂ : β i) :
    nndist (toLp p (Pi.single i b₁)) (toLp p (Pi.single i b₂)) = nndist b₁ b₂ := by
  rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← toLp_sub, ← Pi.single_sub, nnnorm_toLp_single]

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