wSameSide_vadd_right_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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