sOppSide_smul_vsub_vadd_right — Mathlib

English

If x ∉ s, p1,p2 ∈ s and t < 0, then s.SOppSide x (t (x − p1) + p2).

Русский

Если x ∉ s, p1,p2 ∈ s и t < 0, то s.SOppSide x (t (x − p1) + p2).

LaTeX

$$$\forall s \subseteq P,\ x \notin s,\ p_1,p_2 \in s,\ t<0:\ s.SOppSide\bigl(x,\ t\,(x - p_1) + p_2\bigr).$$$

Lean4

theorem sOppSide_smul_vsub_vadd_right {s : AffineSubspace R P} {x p₁ p₂ : P} (hx : x ∉ s) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
    {t : R} (ht : t < 0) : s.SOppSide x (t • (x -ᵥ p₁) +ᵥ p₂) :=
  (sOppSide_smul_vsub_vadd_left hx hp₁ hp₂ ht).symm

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