edist_eq_iSup — Mathlib

English

For compact α and metric β, the edistance between two continuous maps f,g: α → β equals the supremum over x ∈ α of the edistance between f(x) and g(x): edist(f,g) = ⨆_{x∈α} edist(f(x), g(x)).

Русский

Для компактного пространства α и метрического β расстояние edist между двумя непрерывными отображениями f,g: α → β равняется супремуму по x∈α от edist(f(x), g(x)).

LaTeX

$$$\mathrm{edist}(f,g) = \sup_{x \in \alpha} \mathrm{edist}(f(x), g(x)).$$$

Lean4

theorem edist_eq_iSup : edist f g = ⨆ (x : α), edist (f x) (g x) := by
  simp [← isometryEquivBoundedOfCompact α β |>.edist_eq f g, BoundedContinuousFunction.edist_eq_iSup]

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