nonpos_iff_eq_zero'

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.nonpos_iff_eq_zero'

English

μ ≤ 0 iff μ = 0.

Русский

μ ≤ 0 тогда и только тогда, когда μ = 0.

LaTeX

$$$ μ \\le 0 \\iff μ = 0 $$$

Lean4

theorem nonpos_iff_eq_zero' : μ ≤ 0 ↔ μ = 0 :=
  μ.zero_le.ge_iff_eq'

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

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

Разделы

Аффилиация

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