English
For any s, x, y, s.WOppSide x y holds if and only if there exists a point p ∈ s with Wbtw between x and p and p and y.
Русский
Для любого s, x, y выполняется: s.WOppSide x y тогда и только тогда, когда существует p ∈ s с такими свойствами, что Wbtw(x,p,y).
LaTeX
$$$$ s.WOppSide x y \iff \exists p \in s\; (Wbtw\; R\; x\; p\; y). $$$$
Lean4
theorem wOppSide_vadd_right_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y := by rw [wOppSide_comm, wOppSide_vadd_left_iff hv, wOppSide_comm]