toFinite_eq_self

Mathlib.MeasureTheory.Measure.WithDensityFinite

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

← MathLib Explorer

English

If μ is a probability measure, then μ.toFinite = μ.

Русский

Если μ является вероятностной мерой, тогда μ.toFinite = μ.

LaTeX

$$$ [\text{IsProbabilityMeasure } μ] \Rightarrow μ^{toFinite} = μ $$$

Lean4

theorem toFinite_eq_self [IsProbabilityMeasure μ] : μ.toFinite = μ :=
  by
  rw [Measure.toFinite, Measure.toFiniteAux, if_pos, ProbabilityTheory.cond_univ]
  infer_instance

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

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

Разделы

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

Аффилиация

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