tendsto_measure_Ioc_atBot — Mathlib

English

Similarly, the map x ↦ μ(Ioc x a) tends to μ(Iic a) as x → atBot.

Русский

Аналогично, x ↦ μ(Ioc(x, a)) стремится к μ(Iic a) при x → atBot.

LaTeX

$$Tendsto (λ x, μ(Ioc x a)) atBot (𝓝 (μ(Iic a)))$$

Lean4

theorem tendsto_measure_Ioc_atBot [Preorder α] [NoMinOrder α] [(atBot : Filter α).IsCountablyGenerated] (μ : Measure α)
    (a : α) : Tendsto (fun x => μ (Ioc x a)) atBot (𝓝 (μ (Iic a))) :=
  by
  rw [← iUnion_Ioc_left]
  exact tendsto_measure_iUnion_atBot (monotone_id.Ioc antitone_const)

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