measure_univ_eq

Mathlib.MeasureTheory.Constructions.Projective

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

← MathLib Explorer

English

For an IsProjectiveLimit μ P, μ univ = P I univ for every I.

Русский

Для проектированного предела μ P верно μ(всe) = P I(всe) для каждого I.

LaTeX

$$$\forall I,\ μ\text{ univ} = P I\text{ univ}.$$$

Lean4

theorem measure_univ_eq (hμ : IsProjectiveLimit μ P) (I : Finset ι) : μ univ = P I univ := by
  rw [← cylinder_univ I, hμ.measure_cylinder _ MeasurableSet.univ]

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

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

Разделы

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

Аффилиация

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