not_isFiniteMeasure_iff

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

English

¬IsFiniteMeasure μ iff μ(univ) = ∞.

Русский

μ не является конечной тогда и только тогда, когда μ(всё множество) = ∞.

LaTeX

$$$\\neg \\text{IsFiniteMeasure}(\\mu) \\iff \\mu(\\mathsf{univ}) = \\infty$$$

Lean4

theorem not_isFiniteMeasure_iff : ¬IsFiniteMeasure μ ↔ μ univ = ∞ := by simp [isFiniteMeasure_iff]

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

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

Разделы

Аффилиация

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