add_norm_nonneg — Mathlib

English

For real-valued bounded continuous f, the function x ↦ f(x) + ||f|| is nonnegative for all x.

Русский

Для вещественной ограниченно непрерывной функции f функция x ↦ f(x) + ||f|| неотрицательна на всей области определения.

LaTeX

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

Lean4

theorem add_norm_nonneg (f : α →ᵇ ℝ) : 0 ≤ f + const _ ‖f‖ :=
  by
  intro x
  simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, coe_zero, Pi.zero_apply, coe_add, const_apply,
    Pi.add_apply]
  linarith [(abs_le.mp (norm_coe_le_norm f x)).1]

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