sbtw_sub_const_iff — Mathlib

English

For all x, y, z ∈ P and any v ∈ P, Sbtw R (x − v) (y − v) (z − v) holds if and only if Sbtw R x y z holds. This expresses translation invariance in the vector space setting.

Русский

Для любых x, y, z ∈ P и любого v ∈ P выполняется Sbtw R (x − v) (y − v) (z − v) ⇔ Sbtw R x y z. Это выражает инвариантность по переносу векторного пространства.

LaTeX

$$$Sbtw R (x - v) (y - v) (z - v) \iff Sbtw R x y z$$$

Lean4

@[simp]
theorem sbtw_sub_const_iff {x y z : V} (v : V) : Sbtw R (x - v) (y - v) (z - v) ↔ Sbtw R x y z :=
  sbtw_vsub_const_iff v

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