Iio

Mathlib.Order.Interval.Set.Defs

URI: https://scilib.ai/kg/mathlib#Set.Iio

English

The left-infinite right-open interval Iio(b) is the set {x | x < b}.

Русский

Леволинейный правый открытый интервал Iio(b) — множество {x | x < b}.

LaTeX

$$$Iio(b) = \{x \mid x < b\}$$$

Lean4

/-- `Iio b` is the left-infinite right-open interval $(-∞, b)$. -/
def Iio (b : α) :=
  {x | x < b}

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

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

Разделы

Аффилиация

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