wOppSide_lineMap_left — Mathlib

English

For s ∈ AffineSubspace, and x ∈ P, y ∈ P, and t ≤ 0, s.WOppSide (lineMap x y t) y.

Русский

Для s ∈ AffineSubspace и точек x,y ∈ P и t ≤ 0 выполняется: s.WOppSide(lineMap x y t, y).

LaTeX

$$$\forall s:\text{AffineSubspace } R P\ ,\forall x,y\in P\ ,\forall t\in R\ , t\le 0\Rightarrow s.WOppSide(\mathrm{lineMap}(x,y,t), y).$$$

Lean4

theorem wOppSide_lineMap_left {s : AffineSubspace R P} {x : P} (y : P) (h : x ∈ s) {t : R} (ht : t ≤ 0) :
    s.WOppSide (lineMap x y t) y :=
  wOppSide_smul_vsub_vadd_left y h h ht

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