indicator_const_smul — Mathlib

English

The indicator of r • f equals the function that at each point multiplies the indicator of f by r at that point.

Русский

Индикатор r • f равен функция, которая в каждой точке умножает индикатор f на r в этой точке.

LaTeX

$$$ \mathrm{indicator}(s, (a \mapsto r(a) \cdot f(a))) = (a \mapsto r(a)) \cdot \mathrm{indicator}(s, f)(a) $$$

Lean4

theorem indicator_const_smul (s : Set α) (r : R) (f : α → M) : indicator s (r • f ·) = (r • indicator s f ·) :=
  funext <| indicator_const_smul_apply s r f

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