left_mem_affineSegment

Mathlib.Analysis.Convex.Between

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

English

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

Русский

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

LaTeX

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

Lean4

theorem left_mem_affineSegment (x y : P) : x ∈ affineSegment R x y :=
  ⟨0, Set.left_mem_Icc.2 zero_le_one, lineMap_apply_zero _ _⟩

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

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

Разделы

Аффилиация

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