Wbtw

Mathlib.Analysis.Convex.BetweenList

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

English

For any x,y ∈ P, the triple (y, x, pointReflection_R(x)(y)) forms a weak betweenness configuration.

Русский

Для любых x,y ∈ P тройка (y, x, pointReflection_R(x)(y)) образует слабое между.

LaTeX

$$$Wbtw_R y x (\text{pointReflection}_R x y)$$$

Lean4

/-- The points in a list are weakly in that order on a line. -/
protected def Wbtw (l : List P) : Prop :=
  l.Triplewise (Wbtw R)

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

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

Разделы

Аффилиация

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