right_mem_image_Ici_of_left_ne — Mathlib

English

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

Русский

Sbtw эквивалентен x ≠ y и z принадлежит изображению Ioi через прямую x–y.

LaTeX

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

Lean4

theorem right_mem_image_Ici_of_left_ne {x y z : P} (h : Wbtw R x y z) (hne : x ≠ y) :
    z ∈ lineMap x y '' Set.Ici (1 : R) :=
  (wbtw_iff_left_eq_or_right_mem_image_Ici.1 h).resolve_left hne

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