instDist — Mathlib

English

The uniform distance between two bounded continuous functions is defined as the infimum of all nonnegative bounds that bound pointwise distances.

Русский

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

LaTeX

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

Lean4

/-- The uniform distance between two bounded continuous functions. -/
instance instDist : Dist (α →ᵇ β) :=
  ⟨fun f g => sInf {C | 0 ≤ C ∧ ∀ x : α, dist (f x) (g x) ≤ C}⟩

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