Ici

Mathlib.Order.Interval.Set.Defs

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

English

The interval Ici(a) is the left-closed right-infinite interval [a, ∞).

Русский

Интервал Ici(a) — левополузначенный, правополинтервал бесконечности: [a, ∞).

LaTeX

$$$Ici(a) = \{x \mid a \le x\}$$$

Lean4

/-- `Ici a` is the left-closed right-infinite interval $[a, ∞)$. -/
def Ici (a : α) :=
  {x | a ≤ x}

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

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

Разделы

Аффилиация

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