wSameSide_smul_vsub_vadd_right — Mathlib

English

Under the same hypotheses as the previous result but swapping the roles of the two arguments, for any x ∈ P, p1,p2 ∈ s with ht ≥ 0, we have s.WSameSide x (t·(x − p1) + p2).

Русский

При тех же предположениях, что и в предыдущем результате, но поменяв местами аргументы, для любого x ∈ P и p1,p2 ∈ s с ht ≥ 0 верно: s.WSameSide x( t·(x − p1) + p2 ).

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\mathrm{WSameSide}\,x\,(t\cdot (x - p_1) + p_2).$$$

Lean4

theorem wSameSide_smul_vsub_vadd_right {s : AffineSubspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
    {t : R} (ht : 0 ≤ t) : s.WSameSide x (t • (x -ᵥ p₁) +ᵥ p₂) :=
  (wSameSide_smul_vsub_vadd_left x hp₁ hp₂ ht).symm

Похожие утверждения