upper_bound — Mathlib

English

For f ∈ α →ᵇ ℝ≥0 and x ∈ α, f(x) ≤ nndist f 0.

Русский

Для f ∈ α →ᵇ ℝ≥0 и x ∈ α выполняется f(x) ≤ nndist(f, 0).

LaTeX

$$$upper\\_bound\\ (f:\\alpha \\to^{\\mathrm{b}} \\mathbb{R}_{\\ge 0})\\ (x:\\alpha)$$$

Lean4

theorem upper_bound {α : Type*} [TopologicalSpace α] (f : α →ᵇ ℝ≥0) (x : α) : f x ≤ nndist f 0 :=
  by
  have key : nndist (f x) ((0 : α →ᵇ ℝ≥0) x) ≤ nndist f 0 := @dist_coe_le_dist α ℝ≥0 _ _ f 0 x
  simp only [coe_zero, Pi.zero_apply] at key
  rwa [NNReal.nndist_zero_eq_val' (f x)] at key

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