English
For any x, y, ¬Sbtw R x y x, i.e., a point cannot be between itself and another with the same first and last slot.
Русский
Для любых x, y не выполняется Sbtw R x y x; точка не может быть между самой собой и другой точкой.
LaTeX
$$Not (Sbtw R x y x)$$
Lean4
theorem sbtw_iff_mem_image_Ioo_and_ne [NoZeroSMulDivisors R V] {x y z : P} :
Sbtw R x y z ↔ y ∈ lineMap x z '' Set.Ioo (0 : R) 1 ∧ x ≠ z :=
by
refine ⟨fun h => ⟨h.mem_image_Ioo, h.left_ne_right⟩, fun h => ?_⟩
rcases h with ⟨⟨t, ht, rfl⟩, hxz⟩
refine ⟨⟨t, Set.mem_Icc_of_Ioo ht, rfl⟩, ?_⟩
rw [lineMap_apply, ← @vsub_ne_zero V, ← @vsub_ne_zero V _ _ _ _ z, vadd_vsub_assoc, vsub_self, vadd_vsub_assoc, ←
neg_vsub_eq_vsub_rev z x, ← @neg_one_smul R, ← add_smul, ← sub_eq_add_neg]
simp [sub_eq_zero, ht.1.ne.symm, ht.2.ne, hxz.symm]
