tendsto_measure_iInter_atTop — Mathlib

English

Let s(i) be a family of measurable sets indexed by a directed poset with finite-measure at some index; then the limit of μ(⋂_{j≤i} s(j)) as i grows equals μ(⋂_i s(i)).

Русский

Пусть {s(i)} — семейство измеримых множеств с существованием индекса, где мера конечна; тогда предел μ(⋂_{j≤i} s(j)) стремится к μ(⋂_i s(i)).

LaTeX

$$$$\forall i,\ NullMeasurableSet(s(i),\mu) \Rightarrow \mathrm{Tendsto}(\lambda i. μ(\bigcap_{j\le i} s(j)))\ atTop\ (\mathcal{N}(μ(\bigcap_i s(i)))).$$$$

Lean4

/-- Continuity from above: the measure of the intersection of a decreasing sequence of measurable
sets is the limit of the measures. -/
theorem tendsto_measure_iInter_atTop [Preorder ι] [IsCountablyGenerated (atTop : Filter ι)] {s : ι → Set α}
    (hs : ∀ i, NullMeasurableSet (s i) μ) (hm : Antitone s) (hf : ∃ i, μ (s i) ≠ ∞) :
    Tendsto (μ ∘ s) atTop (𝓝 (μ (⋂ n, s n))) :=
  by
  refine .of_neBot_imp fun h ↦ ?_
  have := (atTop_neBot_iff.1 h).2
  rw [hm.measure_iInter hs hf]
  exact tendsto_atTop_iInf fun n m hnm => measure_mono <| hm hnm

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