edist_dist — Mathlib

English

The edist between f and g in Lp equals the real number of the distance between f and g: edist f g = ofReal (dist f g).

Русский

Расстояние edist между f и g в Lp равно real-числу расстояния между ними: edist f g = ofReal(dist f g).

LaTeX

$$edist f g = \mathrm{ofReal}(dist f g)$$

Lean4

protected theorem edist_dist (f g : Lp E p μ) : edist f g = .ofReal (dist f g) := by
  rw [edist_def, dist_def, ← eLpNorm_congr_ae (coeFn_sub _ _), ENNReal.ofReal_toReal (eLpNorm_ne_top (f - g))]

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