edist_def — Mathlib

English

The uniform distance between two UniformFun is the supremum over the domain of the pointwise distances.

Русский

Униформная дистанция между двумя отображениями UniformFun равна верхней границе по всем точкам области определения.

LaTeX

$$\operatorname{edist}(f,g) = \sup_{x} \operatorname{edist}(f(x), g(x))$$

Lean4

theorem edist_def (f g : α →ᵤ β) : edist f g = ⨆ x, edist (toFun f x) (toFun g x) :=
  rfl

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