wSameSide_lineMap_left — Mathlib

English

If x ∈ s and y is any point, then for any t ≥ 0, the affine combination lineMap(x,y,t) with y lies on the same side of s as y.

Русский

Если x ∈ s и y произвольна, то при любом t ≥ 0 точка lineMap(x,y,t) и y лежат на одной стороне s.

LaTeX

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

Lean4

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

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