measure_Ioi_pos — Mathlib

English

For any a in a NoMaxOrder space, the open ray Ioi(a) has positive μ-measure for an open-positivity measure μ.

Русский

Для любого a в пространстве без максимального элемента, луч Ioi(a) имеет положительную μ-мера при μ открыто-положительной мере.

LaTeX

$$$[NoMaxOrder X] \\Rightarrow 0 < \\mu(Ioi(a)).$$$

Lean4

theorem measure_Ioi_pos [NoMaxOrder X] (a : X) : 0 < μ (Ioi a) :=
  isOpen_Ioi.measure_pos μ nonempty_Ioi

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