ae_eq_empty_iff_eq

Mathlib.MeasureTheory.Measure.OpenPos

URI: https://scilib.ai/kg/mathlib#IsOpen.ae_eq_empty_iff_eq

English

For an open U, U =ᵐ[μ] ∅ iff U = ∅.

Русский

Для открытого U, U равно ∅ почти по μ тогда и только тогда U = ∅.

LaTeX

$$$\text{IsOpen}(U) \Rightarrow U =^{\mu}_{ae} \emptyset \iff U = \emptyset.$$$

Lean4

theorem _root_.IsOpen.ae_eq_empty_iff_eq (hU : IsOpen U) : U =ᵐ[μ] (∅ : Set X) ↔ U = ∅ := by
  rw [ae_eq_empty, hU.measure_zero_iff_eq_empty]

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

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

Разделы

Аффилиация

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