sbtw_const_add_iff — Mathlib

English

The equivalence with const add holds: Wbtw R (instHAdd.hAdd v x) (instHAdd.hAdd v y) (instHAdd.hAdd v z) iff Wbtw R x y z.

Русский

С точностью до константного добавления: Wbtw R (x+v) (y+v) (z+v) эквивалентно Wbtw R x y z.

LaTeX

$$Wbtw R (instHAdd.hAdd v x) (instHAdd.hAdd v y) (instHAdd.hAdd v z) \iff Wbtw R x y z$$

Lean4

@[simp]
theorem sbtw_const_add_iff {x y z : V} (v : V) : Sbtw R (v + x) (v + y) (v + z) ↔ Sbtw R x y z :=
  sbtw_const_vadd_iff v

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