mem_affineSpan

Mathlib.Analysis.Convex.Between

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

← MathLib Explorer

English

If h is a Wbtw triple, then y belongs to the affine line determined by x and z.

Русский

Если h задаёт тройку Wbtw, то y принадлежит аффинной прямой, определяемой точками x и z.

LaTeX

$$$y \in \operatorname{line}[R, x, z]$$$

Lean4

theorem mem_affineSpan {x y z : P} (h : Wbtw R x y z) : y ∈ line[R, x, z] :=
  by
  rcases h with ⟨r, ⟨-, rfl⟩⟩
  exact lineMap_mem_affineSpan_pair _ _ _

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

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

Разделы

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

Аффилиация

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