English
An equivalent formulation of the previous statement: translating x by v in s.direction preserves the SOppSide relation with y.
Русский
Эквивалентная формулировка предыдущего: перенос x по v в направлении s сохраняет SOppSide относительно y.
LaTeX
$$$$ s.SOppSide (v +ᵥ x) y \iff s.SOppSide x y, \quad v \in s.direction. $$$$
Lean4
theorem sOppSide_vadd_right_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y := by rw [sOppSide_comm, sOppSide_vadd_left_iff hv, sOppSide_comm]