tendsto_mulIndicator_biUnion_finset

English

The tendsto result for Finset unions shows convergence to the full iUnion indicator under atTop.

Русский

Предел для объединений по Finset демонстрирует схождение к индикатору полного iUnion при atTop.

LaTeX

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

Lean4

@[to_additive]
theorem tendsto_mulIndicator_biUnion_finset {ι} [One β] (s : ι → Set α) (f : α → β) (a : α) :
    Tendsto (fun n : Finset ι => mulIndicator (⋃ i ∈ n, s i) f a) atTop (pure <| mulIndicator (iUnion s) f a) :=
  tendsto_pure.2 <| mulIndicator_biUnion_finset_eventuallyEq s f a

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