mulIndicator_biUnion_apply — Mathlib

English

For s, t, f with pairwise disjoint t over s, the value at x of the union indicator equals the product over i of the indicator at x.

Русский

При попарном непересечении t(i) над i∈s, значение индикатора объединения в точке x равно произведению индикаторов по i.

LaTeX

$$$\forall x,\ mulIndicator (\bigcup i \in s, t(i))\, f\, x = \prod i \in s, mulIndicator (t(i))\, f\, x$$$

Lean4

@[to_additive]
theorem mulIndicator_biUnion_apply (s : Finset ι) (t : ι → Set κ) {f : κ → β} (h : (s : Set ι).PairwiseDisjoint t)
    (x : κ) : mulIndicator (⋃ i ∈ s, t i) f x = ∏ i ∈ s, mulIndicator (t i) f x := by rw [mulIndicator_biUnion s t h]

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