iUnionNotConvergentSeq_subset — Mathlib

English

The union of notConvergentSeq across i is contained in s.

Русский

Объединение по i содержится в s.

LaTeX

$$$\text{iUnionNotConvergentSeq } hε hf hg hsm hs hfg ⊆ s$.$$

Lean4

theorem iUnionNotConvergentSeq_subset (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))) :
    iUnionNotConvergentSeq hε hf hg hsm hs hfg ⊆ s :=
  by
  rw [iUnionNotConvergentSeq, ← Set.inter_iUnion]
  exact Set.inter_subset_left

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