cIcc — Mathlib

English

The closed circular interval between a and b is the set of all x that lie between a and b in the circular order.

Русский

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

LaTeX

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

Lean4

/-- Closed-closed circular interval -/
def cIcc (a b : α) : Set α :=
  {x | btw a x b}

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