edist_comm — Mathlib

English

The edistance is symmetric: edist(f,g) = edist(g,f).

Русский

Расстояние в эвклидовом виде симметрично: edist(f,g) = edist(g,f).

LaTeX

$$$$edist(f,g)=edist(g,f)$$$$

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_comm (f g : PiLp p β) : edist f g = edist g f :=
  by
  rcases p.trichotomy with (rfl | rfl | h)
  · simp only [edist_eq_card, edist_comm]
  · simp only [edist_eq_iSup, edist_comm]
  · simp only [edist_eq_sum h, edist_comm]

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