sOppSide_vadd_right_iff — Mathlib

English

An equivalent formulation of the previous statement: translating x by v in s.direction preserves the SOppSide relation with y.

Русский

Эквивалентная формулировка предыдущего: перенос x по v в направлении s сохраняет SOppSide относительно y.

LaTeX

$$$$ s.SOppSide (v +ᵥ x) y \iff s.SOppSide x y, \quad v \in s.direction. $$$$

Lean4

theorem sOppSide_vadd_right_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
    s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y := by rw [sOppSide_comm, sOppSide_vadd_left_iff hv, sOppSide_comm]

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