Sbtw

Mathlib.Analysis.Convex.BetweenList

URI: https://scilib.ai/kg/mathlib#List.Sbtw

English

A list is strictly between if it is Wbtw and its consecutive elements are pairwise distinct.

Русский

Список строго между, если он Wbtw и пары соседних элементов различны.

LaTeX

$$$\text{List.Sbtw}_R(l) \iff (l.Wbtw R) \land (l.Pairs (\neq))$$$

Lean4

/-- The points in a list are strictly in that order on a line. -/
protected def Sbtw (l : List P) : Prop :=
  l.Wbtw R ∧ l.Pairwise (· ≠ ·)

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

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

Разделы

Аффилиация

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