wOppSide_smul_vsub_vadd_right — Mathlib

English

Symmetric version of the left-scale statement: s.WOppSide x (t·(x − p1) + p2) for t ≤ 0.

Русский

Симметричная версия левого утверждения: s.WOppSide x (t·(x − p1) + p2) при t ≤ 0.

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 x (t\cdot (x - p_1) + p_2).$$$

Lean4

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

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