tendsto_measure_iInter_atBot — Mathlib

English

Dual statement of above: if s(i) is monotone, the limit of μ(s(i)) from below equals μ(⋂ i s(i)).

Русский

Двойственная формулировка: если s(i) монотонно растёт, предел μ(s(i)) снизу равен μ(⋂ i s(i)).

LaTeX

$$$$\text{Monotone}(s) \Rightarrow \ \mathrm{Tendsto}(\mu\circ s)\ atBot\ (\mathcal{N}(μ(\bigcap_n s_n))).$$$$

Lean4

/-- Continuity from above: the measure of the intersection of an increasing sequence of measurable
sets is the limit of the measures. -/
theorem tendsto_measure_iInter_atBot [Preorder ι] [IsCountablyGenerated (atBot : Filter ι)] {s : ι → Set α}
    (hs : ∀ i, NullMeasurableSet (s i) μ) (hm : Monotone s) (hf : ∃ i, μ (s i) ≠ ∞) :
    Tendsto (μ ∘ s) atBot (𝓝 (μ (⋂ n, s n))) :=
  tendsto_measure_iInter_atTop (ι := ιᵒᵈ) hs hm.dual_left hf

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