mulIndicator_biUnion_finset_eventuallyEq

English

For finite unions over Finset, the germ-indicator of the union converges to the germ-indicator of the infinite union, via atTop, mirroring the Monotone case.

Русский

Для конечного объединения по Finset индикатор Г germ сходится к индикатору бесконечного объединения, через atTop.

LaTeX

$$$(\\forall n: Finset ι)\\; (\\bigcup_{i∈n} s_i).mulIndicator f a$ tends to $(\\bigcup_i s_i).mulIndicator f a$$$

Lean4

@[to_additive]
theorem mulIndicator_biUnion_finset_eventuallyEq {ι} [One β] (s : ι → Set α) (f : α → β) (a : α) :
    (fun n : Finset ι => mulIndicator (⋃ i ∈ n, s i) f a) =ᶠ[atTop] fun _ ↦ mulIndicator (iUnion s) f a :=
  by
  rw [iUnion_eq_iUnion_finset s]
  apply Monotone.mulIndicator_eventuallyEq_iUnion
  exact fun _ _ ↦ biUnion_subset_biUnion_left

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