English
Let R be a ring with a compatible order, V a vector space, and x, y, z ∈ V. For every v ∈ V, the relation Sbtw R (v − x) (v − y) (v − z) holds if and only if Sbtw R x y z holds. In other words, the Sbtw predicate is preserved under translation by a fixed vector.
Русский
Пусть R — кольцо с упорядочением, V — векторное пространство, и x, y, z ∈ V. Для любого v ∈ V выражение Sbtw R (v − x) (v − y) (v − z) выполняется тогда и только тогда, когда Sbtw R x y z выполняется. Иными словами, предикат Sbtw сохраняется при сдвиге на фиксированное векторное смещение.
LaTeX
$$$Sbtw R (v - x) (v - y) (v - z) \iff Sbtw R x y z$$$
Lean4
@[simp]
theorem sbtw_const_sub_iff {x y z : V} (v : V) : Sbtw R (v - x) (v - y) (v - z) ↔ Sbtw R x y z :=
sbtw_const_vsub_iff v
