mulIndicator_union_eventuallyEq — Mathlib

English

For a finite union indexed by a Finset, the indicator of the union equals the product of indicators, in the germ sense, matching the infinite union via finset approximations.

Русский

Для конечного объединения по индексу Finset индикатор объединения равен произведению индикаторов в смысле Germ, согласуясь с бесконечным объединением при аппроксимациях Finset.

LaTeX

$$$ (\\bigcup_{i \\in n} s_i).mulIndicator f = (\\bigcup_i s_i).mulIndicator f$ in Germ sense for Finset n$$

Lean4

@[to_additive]
theorem mulIndicator_union_eventuallyEq (h : ∀ᶠ a in l, a ∉ s ∩ t) :
    mulIndicator (s ∪ t) f =ᶠ[l] mulIndicator s f * mulIndicator t f :=
  h.mono fun _a ha => mulIndicator_union_of_notMem_inter ha _

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