nnnorm_indicator_eq_indicator_nnnorm

English

The nnnorm of an indicator equals the indicator of the nnnorm: ‖indicator s f a‖₊ = indicator s (‖f a‖₊) a.

Русский

nnnorm индикатора равен индикатору nnnorm от f: ‖indicator s f a‖₊ = indicator s (‖f a‖₊) a.

LaTeX

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

Lean4

theorem nnnorm_indicator_eq_indicator_nnnorm : ‖indicator s f a‖₊ = indicator s (fun a => ‖f a‖₊) a :=
  flip congr_fun a (indicator_comp_of_zero nnnorm_zero).symm

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