English
If s is an affine subspace and p1,p2 ∈ s, then for x ∈ P and t ≤ 0, s.WOppSide (t·(x − p1) + p2) x.
Русский
Пусть s — аффинное подпространство, p1,p2 ∈ s. Тогда для любого x ∈ P и t ≤ 0, s.WOppSide( t·(x − p1) + p2, x ).
LaTeX
$$$\forall s:\text{AffineSubspace } R P\ ,\forall p_1,p_2\in s\ ,\forall x\in P\ ,\forall t\in R\ , t\le 0\Rightarrow s.WOppSide( t\cdot (x - p_1) + p_2, x).$$$
Lean4
theorem wOppSide_smul_vsub_vadd_left {s : AffineSubspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R}
(ht : t ≤ 0) : s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x :=
by
refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩
rw [vadd_vsub, ← neg_neg t, neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]
exact SameRay.sameRay_nonneg_smul_left _ (neg_nonneg.2 ht)