measureUnivNNReal_eq_zero

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

← MathLib Explorer

English

measureUnivNNReal μ = 0 iff μ = 0 for finite μ.

Русский

measureUnivNNReal μ = 0 эквивалентно μ = 0 при конечной μ.

LaTeX

$$measureUnivNNReal μ = 0 \\iff μ = 0$$

Lean4

@[simp]
theorem measureUnivNNReal_eq_zero [IsFiniteMeasure μ] : measureUnivNNReal μ = 0 ↔ μ = 0 :=
  by
  rw [← MeasureTheory.Measure.measure_univ_eq_zero, ← coe_measureUnivNNReal]
  norm_cast

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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