measure_zero_iff_eq_empty

Mathlib.MeasureTheory.Measure.OpenPos

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

English

For an open U, μ(U) = 0 iff U = ∅.

Русский

Для открытого U, μ(U) = 0 тогда и только тогда U = ∅.

LaTeX

$$$\text{IsOpen}(U) \Rightarrow μ(U) = 0 \iff U = ∅.$$$

Lean4

theorem _root_.IsOpen.measure_zero_iff_eq_empty (hU : IsOpen U) : μ U = 0 ↔ U = ∅ :=
  ⟨fun h ↦ (hU.measure_eq_zero_iff μ).mp h, fun h ↦ by simp [h]⟩

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

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

Разделы

Аффилиация

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