dist_le — Mathlib

English

For nonnegative C, dist f g ≤ C if and only if ∀ x, dist(f(x), g(x)) ≤ C.

Русский

Для неотрицательного C верно: dist f g ≤ C ⇔ ∀ x, dist(f(x), g(x)) ≤ C.

LaTeX

$$$\text{dist\_le}(C_0) : \ dist f g \le C \iff \forall x, \ dist(f(x), g(x)) \le C$$$

Lean4

/-- The distance between two functions is controlled by the supremum of the pointwise distances. -/
theorem dist_le (C0 : (0 : ℝ) ≤ C) : dist f g ≤ C ↔ ∀ x : α, dist (f x) (g x) ≤ C := by
  simp only [← dist_mkOfCompact, BoundedContinuousFunction.dist_le C0, mkOfCompact_apply]

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