nndist_eq_iSup — Mathlib

English

The nonnegative distance between f and g equals the supremum of the pointwise nonnegative distances: nndist f g = ⨆ x : α, nndist (f x) (g x).

Русский

Неотрицательное расстояние между f и g равно супремуму по точкам: nndist f g = ⨆ x, nndist (f x) (g x).

LaTeX

$$$\\operatorname{nndist} f g = \\sup_{x \\in \\alpha} \\operatorname{nndist}(f x, g x).$$$

Lean4

theorem nndist_eq_iSup : nndist f g = ⨆ x : α, nndist (f x) (g x) :=
  Subtype.ext <| dist_eq_iSup.trans <| by simp_rw [val_eq_coe, coe_iSup, coe_nndist]

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