wSameSide_lineMap_right — Mathlib

English

Symmetric version of the previous: for all t ≥ 0, s.WSameSide y lineMap(x,y,t).

Русский

Симметричная версия предыдущего: для всех t ≥ 0, s.WSameSide y lineMap(x,y,t).

LaTeX

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

Lean4

theorem wSameSide_lineMap_right {s : AffineSubspace R P} {x : P} (y : P) (h : x ∈ s) {t : R} (ht : 0 ≤ t) :
    s.WSameSide y (lineMap x y t) :=
  (wSameSide_lineMap_left y h ht).symm

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