sSameSide_lineMap_right — Mathlib

English

If x ∈ s and y ∉ s, with t > 0, then the same line point near y satisfies: s.SSameSide y (lineMap x y t).

Русский

Если x ∈ s и y ∉ s, и t > 0, то точка на прямой, приближенная к y, удовлетворяет: s.SSameSide y (lineMap x y t).

LaTeX

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

Lean4

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

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