indicator_norm_le_norm_self — Mathlib

English

For any a, the value indicator_s (‖f(a)‖) at a is at most ‖f(a)‖; i.e., the indicator of the norm is never larger than the norm itself.

Русский

Для каждого a значение индикатора по ‖f(a)‖ не превосходит ‖f(a)‖; то есть индикация нормы не превышает саму норму.

LaTeX

$$$ \\mathbf{1}_s(a) \\; \\|f(a)\\| \\le \\|f(a)\\| $$$

Lean4

theorem indicator_norm_le_norm_self : indicator s (fun a => ‖f a‖) a ≤ ‖f a‖ :=
  indicator_le_self' (fun _ _ => norm_nonneg _) a

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