indicator_enorm_le_enorm_self — Mathlib

English

For any s and f, the indicator ENORM is bounded by the ENORM of f: ||indicator s f a|| ≤ ||f a||.

Русский

Для любого s и f индуцированная ENORM ограничена ENORM от f: ||indicator s f a|| ≤ ||f a||.

LaTeX

$$$ \| \mathbf{1}_s f(a) \|_\varepsilon \le \| f(a) \|_\varepsilon.$$$

Lean4

theorem indicator_enorm_le_enorm_self : indicator s (fun a => ‖f a‖ₑ) a ≤ ‖f a‖ₑ :=
  indicator_le_self' (fun _ _ ↦ zero_le _) a

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