sOppSide_vadd_left_iff — Mathlib

English

Translating the left argument by a vector in the direction of s does not affect the SOppSide relation with the right argument.

Русский

Смещение левого аргумента на вектор, лежащий на направлении s, не меняет отношение SOppSide относительно правого аргумента.

LaTeX

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

Lean4

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

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