left_mem_image_Ioi — Mathlib

English

If x, y, z satisfy the betweenness Sbtw_R(x, y, z), then the left point x lies on the line through z and y beyond y; that is, x ∈ lineMap(z, y)''(Ioi(1)).

Русский

Если x, y, z удовлетворяют отношению между Sbtw_R(x, y, z), то левая точка x лежит на прямой через z и y за пределами y; то есть x ∈ lineMap(z, y)''(Ioi(1)).

LaTeX

$$$\,\forall x,y,z.\ (Sbtw_R(x,y,z) \Rightarrow x \in lineMap(z,y) '' \mathrm{Ioi}(1))$$$

Lean4

theorem left_mem_image_Ioi {x y z : P} (h : Sbtw R x y z) : x ∈ lineMap z y '' Set.Ioi (1 : R) :=
  h.symm.right_mem_image_Ioi

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