mulIndicator_eventuallyEq_iUnion — Mathlib

English

If a family s(i) is monotone/antitone in i and f is a function, then the germ-based indicators tend to the indicator of the union or intersection, depending on monotonicity, with Tendsto toward pure germ values.

Русский

Если семейство s(i) монотонно или антимонотонно по i, то индикаторы Germ-сообщений стремятся к индикатору объединения или пересечения соответственно, с пределом к чистым значениями.

LaTeX

$$$\\text{Tendsto} (i ↦ (s_i).mulIndicator f a)_{i \\to \\infty} \\; (\\text{towards } (\\bigcup_i s_i).mulIndicator f a)$$$

Lean4

@[to_additive]
theorem mulIndicator_eventuallyEq_iUnion {ι} [Preorder ι] [One β] (s : ι → Set α) (hs : Monotone 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_iUnion f 1 a

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