norm_indicator_eq_indicator_norm — Mathlib

English

The norm of an indicator equals the indicator of the norm: ||indicator s f a|| = indicator s (||f a||) a.

Русский

Норма индикатора равна индикатору нормы: ||indicator s f a|| = indicator s (||f a||) a.

LaTeX

$$$ \| \mathbf{1}_s f(a) \| = \mathbf{1}_s( \| f(a) \| ).$$$

Lean4

theorem norm_indicator_eq_indicator_norm : ‖indicator s f a‖ = indicator s (fun a => ‖f a‖) a :=
  flip congr_fun a (indicator_comp_of_zero norm_zero).symm

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