norm_indicator_le_of_subset — Mathlib

English

Let s ⊆ t be subsets of a set A and f: A → E. Then for every a ∈ A, the norm of the s-indicator of f at a is bounded above by the norm of the t-indicator of f at a: ||1_s(a) f(a)|| ≤ ||1_t(a) f(a)||.

Русский

Пусть s ⊆ t — подмножества множества A и f: A → E. Тогда для каждого a ∈ A выполняется неравенство: ||1_s(a) f(a)|| ≤ ||1_t(a) f(a)||.

LaTeX

$$$ s \\subseteq t \\Rightarrow \\forall a, \\| \\mathbf{1}_s(a) f(a) \\| \\le \\| \\mathbf{1}_t(a) f(a) \\| $$$

Lean4

theorem norm_indicator_le_of_subset (h : s ⊆ t) (f : α → E) (a : α) : ‖indicator s f a‖ ≤ ‖indicator t f a‖ :=
  by
  simp only [norm_indicator_eq_indicator_norm]
  exact indicator_le_indicator_of_subset ‹_› (fun _ => norm_nonneg _) _

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