English
If the set {x, y, z} is collinear, then at least one of the triples (x, y, z), (y, z, x), (z, x, y) is weakly between.
Русский
Если множество {x, y, z} коллинеарно, тогда хотя бы одна из троек (x, y, z), (y, z, x), (z, x, y) образует слабое между.
LaTeX
$$$\text{Collinear}(R, {x,y,z}) \Rightarrow (Wbtw_R x y z \lor Wbtw_R y z x \lor Wbtw_R z x y)$$$
Lean4
theorem collinear {x y z : P} (h : Wbtw R x y z) : Collinear R ({ x, y, z } : Set P) :=
by
rw [collinear_iff_exists_forall_eq_smul_vadd]
refine ⟨x, z -ᵥ x, ?_⟩
intro p hp
simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp
rcases hp with (rfl | rfl | rfl)
· refine ⟨0, ?_⟩
simp
· rcases h with ⟨t, -, rfl⟩
exact ⟨t, rfl⟩
· refine ⟨1, ?_⟩
simp
