apply_le_nndist_zero — Mathlib

English

For any X and a bounded continuous function f: X → ℝ≥0, we have pointwise bound f(x) ≤ distance(0, f) in NNReal for all x.

Русский

Для любой X и ограниченной непрерывной функции f: X → ℝ≥0 выполняется неравенство f(x) ≤ расстояние(0, f) по метрике NNReal для всех x.

LaTeX

$$$$\\forall x,\\; f(x) \\le d_{\\mathrm{NN}}(0, f). $$$$

Lean4

theorem apply_le_nndist_zero {X : Type*} [TopologicalSpace X] (f : X →ᵇ ℝ≥0) (x : X) : f x ≤ nndist 0 f :=
  by
  convert nndist_coe_le_nndist x
  simp only [coe_zero, Pi.zero_apply, NNReal.nndist_zero_eq_val]

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