iUnionNotConvergentSeq_measurableSet

English

The union over all indices i of the sets notConvergentSeq f g n i is measurable provided the hypotheses hold for each i.

Русский

Объединение по всем индексам i множеств notConvergentSeq f g n i является измеримым, если соблюдены предпосылки для каждого i.

LaTeX

$$$\text{MeasurableSet}\bigg(\bigcup_i\, \text{notConvergentSeq } f g n i\bigg)$.$$

Lean4

theorem iUnionNotConvergentSeq_measurableSet (hε : 0 < ε) (hf : ∀ n, StronglyMeasurable (f n))
    (hg : StronglyMeasurable g) (hsm : MeasurableSet s) (hs : μ s ≠ ∞)
    (hfg : ∀ᵐ x ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
    MeasurableSet <| iUnionNotConvergentSeq hε hf hg hsm hs hfg :=
  MeasurableSet.iUnion fun _ => hsm.inter <| notConvergentSeq_measurableSet hf hg

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