mulIndicator_union_mul_inter_apply

English

For any function f and sets s,t, the product of the indicators for s ∪ t and s ∩ t equals the product of the indicators for s and t.

Русский

Для любой функции f и множеств s,t произведение индикаторов для s ∪ t и s ∩ t равно произведению индикаторов для s и t.

LaTeX

$$$$ \operatorname{mulIndicator}(s \cup t) f(a) \cdot \operatorname{mulIndicator}(s \cap t) f(a) = \operatorname{mulIndicator}(s) f(a) \cdot \operatorname{mulIndicator}(t) f(a). $$$$

Lean4

@[to_additive]
theorem mulIndicator_union_mul_inter_apply (f : α → M) (s t : Set α) (a : α) :
    mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a := by
  by_cases hs : a ∈ s <;> by_cases ht : a ∈ t <;> simp [*]

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