indicator_smul_apply_left — Mathlib

English

For any set s and any scalar r, indicator of r • f equals r times indicator f.

Русский

Для любого множества s и скаляра r индикатор r • f равен r на индикатор f.

LaTeX

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

Lean4

theorem indicator_smul_apply_left (s : Set α) (r : α → R) (f : α → M) (a : α) :
    indicator s (fun a ↦ r a • f a) a = indicator s r a • f a :=
  by
  dsimp only [indicator]
  split_ifs
  exacts [rfl, (zero_smul _ (f a)).symm]

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