measure_Iio_pos

Mathlib.MeasureTheory.Measure.OpenPos

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

English

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

Русский

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

LaTeX

$$$[NoMinOrder X] \\Rightarrow 0 < \\mu(Iio(a)).$$$

Lean4

theorem measure_Iio_pos [NoMinOrder X] (a : X) : 0 < μ (Iio a) :=
  isOpen_Iio.measure_pos μ nonempty_Iio

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

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

Разделы

Аффилиация

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