English
Symmetry holds for the relation WS oppSide: s.WOppSide x y iff s.WOppSide y x for any affine subspace s and points x,y.
Русский
Отношение WS OppSide симметрично: s.WOppSide x y ⇔ s.WOppSide y x.
LaTeX
$$$\forall s: \text{AffineSubspace}(R,P)\ \forall x,y: P,\; s.WOppSide\; x\; y \iff s.WOppSide\; y\; x$$$
Lean4
theorem wOppSide_comm {s : AffineSubspace R P} {x y : P} : s.WOppSide x y ↔ s.WOppSide y x :=
by
constructor
· rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩
rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
· rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩
rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
