mulIndicator_mulIndicator — Mathlib

English

For any sets S, T ⊆ α and any function f: α → M, applying the indicator of S to the indicator of T applied to f yields the indicator of S ∩ T applied to f.

Русский

Для множеств S, T ⊆ α и отображения f: α → M применение индикатора S к индикатору T, применённому к f, даёт индикатор S ∩ T применённый к f.

LaTeX

$$$s.mulIndicator (t.mulIndicator f) = (s \\cap t).mulIndicator f$$$

Lean4

@[to_additive]
theorem mulIndicator_mulIndicator (s t : Set α) (f : α → M) :
    mulIndicator s (mulIndicator t f) = mulIndicator (s ∩ t) f :=
  funext fun x => by
    simp only [mulIndicator]
    split_ifs <;> simp_all +contextual

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