sSameSide_vadd_right_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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