left_mem_affineSpan_of_right_ne

Mathlib.Analysis.Convex.Between

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

← MathLib Explorer

English

If Wbtw x y z holds with x ≠ z, then x lies in the affine span of {z, y}.

Русский

Если Wbtw x y z, и x ≠ z, то x лежит в аффинном пространстве, созданном точками z и y.

LaTeX

$$Wbtw(R,x,y,z) → x ∈ affineSpan R { z, y }$$

Lean4

theorem left_mem_affineSpan_of_right_ne {x y z : P} (h : Wbtw R x y z) (hne : z ≠ y) : x ∈ line[R, z, y] :=
  h.symm.right_mem_affineSpan_of_left_ne hne

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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