dist_le — Mathlib

English

If C ≥ 0, then dist f g ≤ C iff ∀ x, dist (f x) (g x) ≤ C.

Русский

Если C ≥ 0, то dist(f,g) ≤ C эквивалентно ∀ x, dist(f(x), g(x)) ≤ C.

LaTeX

$$$0 \le C \Rightarrow (\operatorname{dist}(f,g) \le C \iff \forall x:\alpha, \operatorname{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 :=
  ⟨fun h x => le_trans (dist_coe_le_dist x) h, fun H => csInf_le ⟨0, fun _ => And.left⟩ ⟨C0, H⟩⟩

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