left_mem_affineSpan — Mathlib

English

If x, y, z satisfy Sbtw_R(x, y, z), then x lies on the affine line through z and y; equivalently, x belongs to the affine span of {z, y}.

Русский

Если x, y, z удовлетворяют Sbtw_R(x, y, z), то x лежит на аффинной прямой через z и y; эквивалентно x принадлежит аффинной линее от {z, y}.

LaTeX

$$$Sbtw_R(x,y,z) \Rightarrow x \in \text{affineLine}(z,y) \; (= \text{affineSpan}_R\{z,y\})$$$

Lean4

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

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