indicator_smul_left — Mathlib

English

The indicator of r(a) • f(a) equals the scalar r(a) times the indicator of f(a).

Русский

Индикатор r(a) • f(a) равен r(a) на индикатор f(a).

LaTeX

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

Lean4

theorem indicator_smul_left (s : Set α) (r : α → R) (f : α → M) :
    indicator s (fun a ↦ r a • f a) = fun a ↦ indicator s r a • f a :=
  funext <| indicator_smul_apply_left _ _ _

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