English
Let R be a totally ordered field and x, y, z be points of an affine space over R. The Betweenness relation Sbtw_R(x, y, z) holds exactly when z ≠ y and x lies on the line through z and y beyond y; equivalently, x = lineMap(z, y)(t) for some t > 1.
Русский
Пусть R – упорядоченное поле, и x, y, z – точки аффинного пространства над R. Отношение между Sbtw_R(x, y, z) выполняется тогда и только тогда z ≠ y и x лежит на прямой, проходящей через z и y за пределами y; эквивалентно, существует t > 1 такое, что x = lineMap(z, y)(t).
LaTeX
$$$Sbtw_R(x,y,z) \iff (z \neq y) \land (x \in \ lineMap(z,y) '' \{t \in R \mid t>1\})$$$
Lean4
theorem sbtw_iff_right_ne_and_left_mem_image_Ioi {x y z : P} :
Sbtw R x y z ↔ z ≠ y ∧ x ∈ lineMap z y '' Set.Ioi (1 : R) := by
rw [sbtw_comm, sbtw_iff_left_ne_and_right_mem_image_Ioi]
