tendsto_mulIndicator — Mathlib

English

For a monotone family indexed by Finset or i, tends toward the union, via germ-indicators, in the atTop filter.

Русский

Для монотонной семьи, индексированной конечными множествами, тенденция идёт к объединению через индикаторы Герма в фильтре atTop.

LaTeX

$$$\\text{Tendsto} (\\lambda n. (\\bigcup_{i∈n} s_i).mulIndicator f a)_{n} \\to \\text{pure}((\\bigcup_i s_i).mulIndicator f a)$$$

Lean4

@[to_additive]
theorem tendsto_mulIndicator {ι} [Preorder ι] [One β] (s : ι → Set α) (hs : Monotone s) (f : α → β) (a : α) :
    Tendsto (fun i => mulIndicator (s i) f a) atTop (pure <| mulIndicator (⋃ i, s i) f a) :=
  tendsto_pure.2 <| hs.mulIndicator_eventuallyEq_iUnion s f a

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