right_mem_affineSegment

Mathlib.Analysis.Convex.Between

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

English

The right endpoint y lies in the affine segment between x and y.

Русский

Правый конец y принадлежит афинному отрезку между x и y.

LaTeX

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

Lean4

theorem right_mem_affineSegment (x y : P) : y ∈ affineSegment R x y :=
  ⟨1, Set.right_mem_Icc.2 zero_le_one, lineMap_apply_one _ _⟩

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

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

Разделы

Аффилиация

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