eventually

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

← MathLib Explorer

English

If μ.FiniteAtFilter f then μ.FiniteAtFilter (f ⊔ g).

Русский

Если μ конечна на фильтре f, тогда конечна на их объединении f ⊔ g.

LaTeX

$$$\exists$ … (finite at filter of supremum)$$

Lean4

protected theorem eventually (h : μ.FiniteAtFilter f) : ∀ᶠ s in f.smallSets, μ s < ∞ :=
  (eventually_smallSets' fun _s _t hst ht => (measure_mono hst).trans_lt ht).2 h

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

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

Разделы

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

Аффилиация

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