sbtw_const_vsub_iff — Mathlib

English

Under a constant affine addition, Sbtw is preserved: Sbtw R (instHVAdd.hVAdd x p) (instHVAdd.hVAdd y p) (instHVAdd.hVAdd z p) iff Sbtw R x y z.

Русский

При добавлении константы в аффинном действии сохраняется Sbtw.

LaTeX

$$Sbtw R (instHVAdd.hVAdd x p) (instHVAdd.hVAdd y p) (instHVAdd.hVAdd z p) \iff Sbtw R x y z$$

Lean4

@[simp]
theorem sbtw_const_vsub_iff {x y z : P} (p : P) : Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z := by
  rw [Sbtw, Sbtw, wbtw_const_vsub_iff, (vsub_right_injective p).ne_iff, (vsub_right_injective p).ne_iff]

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