sSameSide_smul_vsub_vadd_right — Mathlib

English

Let s be an affine subspace. If x ∉ s and p1, p2 ∈ s and t > 0, then the same conclusion holds with the two arguments swapped: s.SSameSide x (t (x − p1) + p2).

Русский

Пусть s — аффинное подпространство. Если x не принадлежит s и p1, p2 ∈ s и t > 0, то выполняется та же работа для пары (x, t (x − p1) + p2): s.SSameSide x (t (x − p1) + p2).

LaTeX

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

Lean4

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

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