cIoo

Mathlib.Order.Circular

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

English

The open circular interval between a and b is the set of all x such that sbtw a x b.

Русский

Открытый циклический интервал между a и b — это множество всех x, удовлетворяющих sbtw a x b.

LaTeX

$$$cIoo(a,b) = \{ x \in \alpha \\mid \\mathrm{sbtw}(a,x,b) \}.$$$

Lean4

/-- Open-open circular interval -/
def cIoo (a b : α) : Set α :=
  {x | sbtw a x b}

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

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

Разделы

Аффилиация

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