indicator_smul_apply — Mathlib

English

The support of the product f • g equals the intersection of the supports of f and g, under suitable conditions.

Русский

Поддержка произведения f • g равна пересечению поддержек f и g при подходящих условиях.

LaTeX

$$$ \operatorname{supp}(f \cdot g) = \operatorname{supp}(f) \cap \operatorname{supp}(g) $$$

Lean4

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

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