English
For any injective affine map f, the property of being weakly on the same side is preserved by passage to the image: (s.map f).WSameSide (f x) (f y) iff s.WSameSide x y.
Русский
Для любого инъективного аффинного отображения f свойство слабого совпадения по одной стороне сохраняется при образе: (s.map f).WSameSide (f x) (f y) эквивалентно s.WSameSide x y.
LaTeX
$$$$ (s.map f) .\mathrm{WSameSide} (f x) (f y) \iff s .\mathrm{WSameSide} x y. $$$$
Lean4
/-- The points `x` and `y` are weakly on the same side of `s`. -/
def WSameSide (s : AffineSubspace R P) (x y : P) : Prop :=
∃ᵉ (p₁ ∈ s) (p₂ ∈ s), SameRay R (x -ᵥ p₁) (y -ᵥ p₂)