English
The pair of relations WSameSide and WOppSide holds together if and only if at least one of the points lies in the affine subspace.
Русский
Сочетание отношений WSameSide и WOppSide выполняется тогда и только тогда, когда хотя бы одна из точек принадлежит аффинному подпространству.
LaTeX
$$$\\\\forall s : \\mathrm{AffineSubspace}\\\\ R P, \\\\forall x y : P, \\\\; (s.WSameSide x y \\\\land s.WOppSide x y) \\\\iff (x \\in s \\\\lor y \\in s)$$$
Lean4
theorem wSameSide_and_wOppSide_iff {s : AffineSubspace R P} {x y : P} :
s.WSameSide x y ∧ s.WOppSide x y ↔ x ∈ s ∨ y ∈ s :=
by
constructor
· rintro ⟨hs, ho⟩
rw [wOppSide_comm] at ho
by_contra h
rw [not_or] at h
exact h.1 (wOppSide_self_iff.1 (hs.trans_wOppSide ho h.2))
· rintro (h | h)
· exact ⟨wSameSide_of_left_mem y h, wOppSide_of_left_mem y h⟩
· exact ⟨wSameSide_of_right_mem x h, wOppSide_of_right_mem x h⟩
