English
Let S be an affine subspace of P. If x and y lie on the same side of S, y and z lie on the weak opposite side of S, and y is 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.SSameSide x y \\\\land\\\\; s.WOppSide y z \\\\land\\\\; y \\\\notin s \\\\Rightarrow s.WOppSide x z$$$
Lean4
theorem trans_wSameSide {s : AffineSubspace R P} {x y z : P} (hxy : s.WOppSide x y) (hyz : s.WSameSide y z)
(hy : y ∉ s) : s.WOppSide x z :=
(hyz.symm.trans_wOppSide hxy.symm hy).symm
