Ico

Mathlib.Order.Interval.Set.Defs

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

English

The half-closed interval Ico(a,b) is the set of x with a ≤ x and x < b; i.e., Ico(a,b) = {x | a ≤ x ∧ x < b}.

Русский

Полуоткрытый интервал Ico(a,b) состоит из x, обладающих a ≤ x и x < b; то есть Ico(a,b) = {x | a ≤ x ∧ x < b}.

LaTeX

$$$Ico(a,b) = \{x \mid a \le x \land x < b\}$$$

Lean4

/-- `Ico a b` is the left-closed right-open interval $[a, b)$. -/
def Ico (a b : α) :=
  {x | a ≤ x ∧ x < b}

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

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

Разделы

Аффилиация

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