enorm_indicator_eq_indicator_enorm

English

For any subset s and function f, the ENORM of the indicator equals the indicator of the ENORM of f.

Русский

Для любого множества s и функции f, ENORM индикатора равен индикатору ENORM от f.

LaTeX

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

Lean4

theorem enorm_indicator_eq_indicator_enorm : ‖indicator s f a‖ₑ = indicator s (fun a => ‖f a‖ₑ) a :=
  flip congr_fun a (indicator_comp_of_zero (enorm_zero (E := ε))).symm

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