sSameSide_vadd_left_iff — Mathlib

English

For any v in the direction of s, s.SSameSide (v +ᵥ x) y iff s.SSameSide x y.

Русский

Для любого v в направлении s: s.SSameSide (v +ᵥ x) y ⇔ s.SSameSide x y.

LaTeX

$$$\forall s: \text{AffineSubspace}(R,P)\ \forall x,y: P\;\forall v\in s.direction,\; s.SSameSide( v +ᵥ x) y \iff s.SSameSide x y$$$

Lean4

theorem sSameSide_vadd_left_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
    s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y := by
  rw [SSameSide, SSameSide, wSameSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]

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