mass_nonzero_iff

Mathlib.MeasureTheory.Measure.FiniteMeasure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.FiniteMeasure.mass_nonzero_iff

English

The mass is nonzero iff the finite measure is nonzero.

Русский

Масса не равна нулю тогда и только тогда пока сама конечная мера не равна нулю.

LaTeX

$$theorem mass_nonzero_iff (μ : FiniteMeasure Ω) : μ.mass ≠ 0 ↔ μ ≠ 0$$

Lean4

theorem mass_nonzero_iff (μ : FiniteMeasure Ω) : μ.mass ≠ 0 ↔ μ ≠ 0 :=
  not_iff_not.mpr <| FiniteMeasure.mass_zero_iff μ

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

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

Разделы

Аффилиация

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