English
Let s be an affine subspace of the ambient affine space P. If x is not in s and p1, p2 lie in s, and t > 0, then the point y = p2 + t (x − p1) lies on the same side of s as x.
Русский
Пусть s — аффинное подпространство в несобщем аффинном пространстве P. Если x не принадлежит s, а точки p1 и p2 принадлежат s, и t > 0, то точка y = p2 + t (x − p1) лежит по ту же сторону от s, что и x.
LaTeX
$$$\forall s \subseteq P,\ x \notin s,\ p_1, p_2 \in s,\ t>0:\ s.SSameSide\bigl(t\,(x - p_1) + p_2,\ x\bigr).$$$
Lean4
theorem sSameSide_smul_vsub_vadd_left {s : AffineSubspace R P} {x p₁ p₂ : P} (hx : x ∉ s) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
{t : R} (ht : 0 < t) : s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x :=
by
refine ⟨wSameSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩
rwa [vadd_mem_iff_mem_direction _ hp₂, s.direction.smul_mem_iff ht.ne.symm, vsub_right_mem_direction_iff_mem hp₁] at h
