isFiniteMeasure

Mathlib.MeasureTheory.Constructions.Projective

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IsProjectiveLimit.isFiniteMeasure

← MathLib Explorer

English

If every P i is finite, then μ is a finite measure.

Русский

Если каждая P i имеет конечную меру, то μ конечна.

LaTeX

$$$[\forall i, IsFiniteMeasure(P i)] \rightarrow IsFiniteMeasure(μ).$$$

Lean4

theorem isFiniteMeasure [∀ i, IsFiniteMeasure (P i)] (hμ : IsProjectiveLimit μ P) : IsFiniteMeasure μ :=
  by
  constructor
  rw [hμ.measure_univ_eq (∅ : Finset ι)]
  exact measure_lt_top _ _

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

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

Разделы

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

Аффилиация

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