English
Let S be an affine subspace of P. If x and y lie on the opposite side of S and y and z lie on the opposite side of S, then x and z lie on the same side of S.
Русский
Пусть S — аффинное подпространство P. Если x и y лежат на противоположной стороне S, а y и z лежат на противоположной стороне S, то x и z лежат на одной стороне S.
LaTeX
$$$\\\\forall s : \\mathrm{AffineSubspace}\\\\ R P, \\\\forall x,y,z : P, \\\\; s.WOppSide x y \\\\land\\\\; s.WOppSide y z \\\\Rightarrow s.WSameSide x z$$$
Lean4
theorem trans {s : AffineSubspace R P} {x y z : P} (hxy : s.WOppSide x y) (hyz : s.WOppSide y z) (hy : y ∉ s) :
s.WSameSide x z := by
rcases hxy with ⟨p₁, hp₁, p₂, hp₂, hxy⟩
rw [wOppSide_iff_exists_left hp₂, or_iff_right hy] at hyz
rcases hyz with ⟨p₃, hp₃, hyz⟩
rw [← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev] at hyz
refine ⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩
refine fun h => False.elim ?_
rw [vsub_eq_zero_iff_eq] at h
exact hy (h ▸ hp₂)
