instIsFiniteMeasureToFinite

Mathlib.MeasureTheory.Measure.WithDensityFinite

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

English

If μ is SFinite, then μ.toFinite is finite, i.e., IsFiniteMeasure μ.toFinite.

Русский

Если μ является SFinite, то μ.toFinite конечна: IsFiniteMeasure μ.toFinite.

LaTeX

$$$ [SFinite \mu] \Rightarrow IsFiniteMeasure(\mu^{toFinite}) $$$

Lean4

instance [SFinite μ] : IsFiniteMeasure μ.toFinite :=
  by
  rw [Measure.toFinite]
  infer_instance

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

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

Разделы

Аффилиация

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