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