sSameSide_lineMap_left — Mathlib

English

If x ∈ s and y ∉ s, and t > 0, then the point on the line from x to y at parameter t lies on the same side as y with respect to s.

Русский

Если x ∈ s и y ∉ s, и t > 0, то точка на прямой от x к y в параметре t лежит на той же стороне от s, что и y.

LaTeX

$$$\forall s \subseteq P,\ x \in s,\ y \notin s,\ t>0:\ s.SSameSide\bigl(\mathrm{lineMap}(x,y,t), y\bigr).$$$

Lean4

theorem sSameSide_lineMap_left {s : AffineSubspace R P} {x y : P} (hx : x ∈ s) (hy : y ∉ s) {t : R} (ht : 0 < t) :
    s.SSameSide (lineMap x y t) y :=
  sSameSide_smul_vsub_vadd_left hy hx hx ht

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