sOppSide_lineMap_right — Mathlib

English

If x ∈ s and y ∉ s and t < 0, then s.SOppSide y (lineMap x y t).

Русский

Если x ∈ s и y ∉ s и t < 0, тогда s.SOppSide y (lineMap x y t).

LaTeX

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

Lean4

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

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