wbtw_iff_right_eq_or_left_mem_image_Ici

English

Wbtw is equivalent to either x = y or z lies in the image of lineMap x y under Ici.

Русский

Wbtw эквивалентно либо x = y, либо z принадлежит образу lineMap x y с Ici.

LaTeX

$$Wbtw(R,x,y,z) ⇔ x = y ∨ z ∈ lineMap x y '' Ici(1)$$

Lean4

theorem wbtw_iff_right_eq_or_left_mem_image_Ici {x y z : P} :
    Wbtw R x y z ↔ z = y ∨ x ∈ lineMap z y '' Set.Ici (1 : R) := by
  rw [wbtw_comm, wbtw_iff_left_eq_or_right_mem_image_Ici]

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