enorm_indicator_le_of_subset — Mathlib

English

If s ⊆ t, then the ENORM of indicator s f a is bounded by the ENORM of indicator t f a.

Русский

Если s⊆t, то ENORM индикатора s f a не превосходит ENORM индикатора t f a.

LaTeX

$$$ s \subseteq t \Rightarrow \| \mathbf{1}_s f(a) \|_\varepsilon \le \| \mathbf{1}_t f(a) \|_\varepsilon.$$$

Lean4

theorem enorm_indicator_le_of_subset (h : s ⊆ t) (f : α → ε) (a : α) : ‖indicator s f a‖ₑ ≤ ‖indicator t f a‖ₑ :=
  by
  simp only [enorm_indicator_eq_indicator_enorm]
  apply indicator_le_indicator_of_subset ‹_› (zero_le _)

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