ae_zero

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

The almost everywhere measure of the zero measure is the bottom element: ae (0) = ⊥.

Русский

Пусть ae (0) = ⊥.

LaTeX

$$ae (0 : Measure α) = ⊥$$

Lean4

@[simp]
theorem ae_zero {_m0 : MeasurableSpace α} : ae (0 : Measure α) = ⊥ :=
  ae_eq_bot.2 rfl

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

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

Разделы

Аффилиация

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