ae_eq_bot

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

ae μ = ⊥ if and only if μ is the zero measure.

Русский

ae μ = ⊥ эквивалентно μ = 0 (нулевая мера).

LaTeX

$$ae μ = ⊥ \iff μ = 0$$

Lean4

@[simp]
theorem ae_eq_bot : ae μ = ⊥ ↔ μ = 0 := by rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]

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

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

Разделы

Аффилиация

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