dist_apply_le_dist — Mathlib

English

For any x ∈ α, the pointwise distance between f(x) and g(x) does not exceed the overall distance between f and g.

Русский

Для любого x ∈ α расстояние между f(x) и g(x) не превосходит общего расстояния между f и g.

LaTeX

$$$\dist(f\,x, g\,x) \leq \dist(f,g)$$$

Lean4

/-- The pointwise distance is controlled by the distance between functions, by definition. -/
theorem dist_apply_le_dist (x : α) : dist (f x) (g x) ≤ dist f g := by
  simp only [← dist_mkOfCompact, dist_coe_le_dist, ← mkOfCompact_apply]

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