tendsto_measure_Ici_atBot

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.tendsto_measure_Ici_atBot

← MathLib Explorer

English

Dual result: μ(Ici x)→μ(univ) as x → atBot.

Русский

Двойственный результат: μ(Ici x) → μ(всё) при x → atBot.

LaTeX

$$Tendsto (λ x, μ(Ici x)) atBot (𝓝 μ(univ))$$

Lean4

theorem tendsto_measure_Ici_atBot [Preorder α] [(atBot : Filter α).IsCountablyGenerated] (μ : Measure α) :
    Tendsto (fun x => μ (Ici x)) atBot (𝓝 (μ univ)) :=
  tendsto_measure_Iic_atTop (α := αᵒᵈ) μ

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru