dist_eq_iSup — Mathlib

English

The distance between f and g is the supremum over x in α of the distances at x: dist f g = ⨆ x : α, dist (f x) (g x).

Русский

Расстояние между f и g равно.supremum по x∈α от расстояния между f(x) и g(x).

LaTeX

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

Lean4

theorem dist_eq_iSup : dist f g = ⨆ x : α, dist (f x) (g x) :=
  by
  cases isEmpty_or_nonempty α
  · rw [iSup_of_empty', Real.sSup_empty, dist_zero_of_empty]
  refine (dist_le_iff_of_nonempty.mpr <| le_ciSup ?_).antisymm (ciSup_le dist_coe_le_dist)
  exact dist_set_exists.imp fun C hC => forall_mem_range.2 hC.2

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