mulIndicator_inter_mulSupport — Mathlib

English

For any set S ⊆ α and any function f: α → M, the indicator of S restricted to the support of f equals the indicator on S.

Русский

Для множества S ⊆ α и функции f: α → M индикатор S по отношению к поддержке функции f равен индикатору на S.

LaTeX

$$$(s \\cap \\operatorname{mulSupport}(f)).mulIndicator f = s.mulIndicator f$$$

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_inter_mulSupport (s : Set α) (f : α → M) : mulIndicator (s ∩ mulSupport f) f = mulIndicator s f :=
  by rw [← mulIndicator_mulIndicator, mulIndicator_mulSupport]

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