sbtw_vadd_const_iff — Mathlib

English

A simplification form of the previous lemma under simp: Wbtw R (instHAdd.hAdd v x) (instHAdd.hAdd v y) (instHAdd.hAdd v z) equals Wbtw R x y z.

Русский

Упрощённая форма предыдущего лема под simp.

LaTeX

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

Lean4

@[simp]
theorem sbtw_vadd_const_iff {x y z : V} (p : P) : Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z := by
  rw [Sbtw, Sbtw, wbtw_vadd_const_iff, (vadd_right_injective p).ne_iff, (vadd_right_injective p).ne_iff]

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