ae_toFinite

Mathlib.MeasureTheory.Measure.WithDensityFinite

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

English

For [SFinite μ], ae μ.toFinite = ae μ; identical almost everywhere statements between μ and its finite form.

Русский

Для [SFinite μ], ae μ.toFinite = ae μ; одинаково почти всюду для μ и ее конечной формы.

LaTeX

$$$ \ae μ.toFinite = \ae μ $$$

Lean4

@[simp]
theorem ae_toFinite [SFinite μ] : ae μ.toFinite = ae μ := by simp [Measure.toFinite, ProbabilityTheory.cond]

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

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

Разделы

Аффилиация

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