edist_self — Mathlib

English

For any f in PiLp p β, edist(f,f) = 0, i.e., distance to itself is zero.

Русский

Для любого f в PiLp p β расстояние до самого себя равно нулю.

LaTeX

$$$$edist(f,f)=0$$$$

Lean4

/-- This holds independent of `p` and does not require `[Fact (1 ≤ p)]`. We keep it separate
from `pi_Lp.pseudo_emetric_space` so it can be used also for `p < 1`. -/
protected theorem edist_self (f : PiLp p β) : edist f f = 0 :=
  by
  rcases p.trichotomy with (rfl | rfl | h)
  · simp [edist_eq_card]
  · simp [edist_eq_iSup]
  · simp [edist_eq_sum h, ENNReal.zero_rpow_of_pos h, ENNReal.zero_rpow_of_pos (inv_pos.2 <| h)]

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