right_mem_affineSpan

Mathlib.Analysis.Convex.Between

URI: https://scilib.ai/kg/mathlib#Sbtw.right_mem_affineSpan

English

Sbtw is equivalent to x ≠ y and z lies in the image of lineMap x y under Ioi.

Русский

Sbtw эквивалентно x ≠ y и z лежит воображении Ioi через lineMap x y.

LaTeX

$$Sbtw(R,x,y,z) ⇔ x ≠ y ∧ z ∈ lineMap x y '' Ioi(1)$$

Lean4

theorem right_mem_affineSpan {x y z : P} (h : Sbtw R x y z) : z ∈ line[R, x, y] :=
  h.wbtw.right_mem_affineSpan_of_left_ne h.left_ne

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

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

Разделы

Аффилиация

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