mulIndicator_eventuallyEq_iInter — Mathlib

English

If s(i) is an antitone family of sets, then the indicators converge to the indicator of the intersection, in the atTop sense.

Русский

Если s(i) образует антитонную семью множеств, индикаторы сходятся к индикатору пересечения в смысле atTop.

LaTeX

$$$\\text{Antitone}(s) \\Rightarrow (\\forall a, (s(i).mulIndicator f a) \\to (\\bigcap_i s_i).mulIndicator f a)$$$

Lean4

@[to_additive]
theorem mulIndicator_eventuallyEq_iInter {ι} [Preorder ι] [One β] (s : ι → Set α) (hs : Antitone s) (f : α → β)
    (a : α) : (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun _ ↦ mulIndicator (⋂ i, s i) f a := by
  classical exact hs.piecewise_eventually_eq_iInter f 1 a

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