English
Translating the left argument by a vector in the direction of s does not affect the SOppSide relation with the right argument.
Русский
Смещение левого аргумента на вектор, лежащий на направлении s, не меняет отношение SOppSide относительно правого аргумента.
LaTeX
$$$$ s.SOppSide (v +\!\! x) y \iff s.SOppSide x y, \quad v \in s.direction. $$$$
Lean4
theorem sOppSide_vadd_left_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y := by
rw [SOppSide, SOppSide, wOppSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]