norm_sub_nonneg — Mathlib

English

The function x ↦ ||f|| − f(x) is nonnegative for all x.

Русский

Функция x ↦ ||f|| − f(x) неотрицательна для всех x.

LaTeX

$$$$\forall x,\; \|f\| - f(x) \ge 0.$$$$

Lean4

theorem norm_sub_nonneg (f : α →ᵇ ℝ) : 0 ≤ const _ ‖f‖ - f :=
  by
  intro x
  simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, coe_zero, Pi.zero_apply, coe_sub, const_apply,
    Pi.sub_apply, sub_nonneg]
  linarith [(abs_le.mp (norm_coe_le_norm f x)).2]

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