sbtw_neg_iff — Mathlib

English

The Sbtw relation is preserved under taking additive inverses: Sbtw R (−x) (−y) (−z) is equivalent to Sbtw R x y z.

Русский

Отражение по противоположной оси сохраняет отношение Sbtw: Sbtw R (−x) (−y) (−z) эквивалентно Sbtw R x y z.

LaTeX

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

Lean4

@[simp]
theorem sbtw_neg_iff {x y z : V} : Sbtw R (-x) (-y) (-z) ↔ Sbtw R x y z := by simp only [← zero_sub, sbtw_const_sub_iff]

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