English
Let s be an affine subspace of the ambient affine space P over a commutative ring R with an R-module structure, and let p1, p2 ∈ s. For any x ∈ P and any t ∈ R with t ≥ 0, the point t·(x − p1) + p2 lies on the same side of s as x, i.e., s implements the same-side relation between t·(x − p1) + p2 and x.
Русский
Пусть s — аффинное подпредложение в заданном аффинном пространстве P над кольцом R; пусть p1, p2 ∈ s. Для любого x ∈ P и любого t ∈ R с t ≥ 0 точка t·(x − p1) + p2 лежит на той же стороне s, что и x, то есть выполняется отношение одной и той же стороны.
LaTeX
$$$\forall s:\text{AffineSubspace } R P\ ,\forall p_1,p_2\in s\ ,\forall x\in P\ ,\forall t\in R\ , t\ge 0\ \Rightarrow\ s\mathrel{\mathrm{WSameSide}}\bigl( t\cdot (x - p_1) + p_2, x \bigr).$$$
Lean4
theorem wSameSide_smul_vsub_vadd_left {s : AffineSubspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R}
(ht : 0 ≤ t) : s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x :=
by
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩
rw [vadd_vsub]
exact SameRay.sameRay_nonneg_smul_left _ ht
