finiteAtFilter_of_finite

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.finiteAtFilter_of_finite

← MathLib Explorer

English

For any μ, μ.FiniteAtFilter ⊥ holds; for example μ(∅) < ∞.

Русский

Для любой μ выполняется μ.FiniteAtFilter ⊥; например μ(∅) < ∞.

LaTeX

$$μ.FiniteAtFilter ⊥$$

Lean4

theorem finiteAtFilter_of_finite {_m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (f : Filter α) :
    μ.FiniteAtFilter f :=
  ⟨univ, univ_mem, measure_lt_top μ univ⟩

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

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

Разделы

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

Аффилиация

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