measure_Ioo_eq_zero

Mathlib.MeasureTheory.Measure.OpenPos

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.measure_Ioo_eq_zero

← MathLib Explorer

English

For densely ordered X, μ(Ioo a b) = 0 iff b ≤ a.

Русский

Для плотно упорядоченного X, μ(Ioo(a,b)) = 0 тогда и только тогда, когда b ≤ a.

LaTeX

$$$[DenselyOrdered X]\\; μ(Ioo(a,b)) = 0 \\iff b \\le a.$$$

Lean4

theorem measure_Ioo_eq_zero [DenselyOrdered X] {a b : X} : μ (Ioo a b) = 0 ↔ b ≤ a :=
  (isOpen_Ioo.measure_eq_zero_iff μ).trans (Ioo_eq_empty_iff.trans not_lt)

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

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

Разделы

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

Аффилиация

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