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