nndist_eq_iSup — Mathlib

English

The nonnegative distance nndist between f and g equals the supremum over x of nndist(f(x), g(x)).

Русский

Нормированная по модулю мера расстояния nndist между f и g равна Sup_x nndist(f(x), g(x)).

LaTeX

$$$\mathrm{nndist}\, f g = \sup_{x} \mathrm{nndist}(f(x), g(x))$$$

Lean4

theorem nndist_eq_iSup : nndist f g = ⨆ x, nndist (f x) (g x) := by
  simp [← isometryEquivBoundedOfCompact α β |>.nndist_eq f g, BoundedContinuousFunction.nndist_eq_iSup]

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