Wbtw

Mathlib.Analysis.Convex.Between

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

English

The endpoint y is contained in the affine segment from x to y (reiterating the standard endpoint property).

Русский

Конец y содержится в афинном отрезке от x к y (повторная констатация свойства концов).

LaTeX

$$$y \in \operatorname{affineSegment}(R,x,y).$$$

Lean4

/-- The point `y` is weakly between `x` and `z`. -/
def Wbtw (x y z : P) : Prop :=
  y ∈ affineSegment R x z

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

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

Разделы

Аффилиация

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