dist_eq — Mathlib

English

The nonnegative distance between f and g (in NNReal) is the infimum of nonnegative bounds that bound pointwise NN distances.

Русский

NNDist между f и g задаётся как инфимум неотрицательных границ, ограничивающих покомпонентные расстояния.

LaTeX

$$$\operatorname{nndist}(f,g) = \inf\{ C \ge 0 \mid \forall x, \operatorname{nndist}(f(x), g(x)) \le C \}$$$

Lean4

theorem dist_eq : dist f g = sInf {C | 0 ≤ C ∧ ∀ x : α, dist (f x) (g x) ≤ C} :=
  rfl

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