tendsto_measure_Iic_atTop — Mathlib

English

For a preorder α with atTop and countable generation, μ(Iic x) tends to μ(univ) as x → atTop.

Русский

Предел функции x ↦ μ(Iic x) при x, стремящемся к бесконечности, равен μ(всё).

LaTeX

$$Tendsto (λ x, μ(Iic x)) atTop (𝓝 μ(univ))$$

Lean4

theorem tendsto_measure_Iic_atTop [Preorder α] [(atTop : Filter α).IsCountablyGenerated] (μ : Measure α) :
    Tendsto (fun x => μ (Iic x)) atTop (𝓝 (μ univ)) :=
  by
  rw [← iUnion_Iic]
  exact tendsto_measure_iUnion_atTop monotone_Iic

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