sbtw_const_vadd_iff — Mathlib

English

For an affine equivalence f, Sbtw R (EquivLike.toFunLike.coe f x) (EquivLike.toFunLike.coe f y) (EquivLike.toFunLike.coe f z) holds iff Sbtw R x y z.

Русский

Для аффинного эквивалента f верно: Sbtw R (f x) (f y) (f z) эквивалентно Sbtw R x y z.

LaTeX

$$Sbtw R (EquivLike.toFunLike.coe f x) (EquivLike.toFunLike.coe f y) (EquivLike.toFunLike.coe f z) \iff Sbtw R x y z$$

Lean4

@[simp]
theorem sbtw_const_vadd_iff {x y z : P} (v : V) : Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z := by
  rw [Sbtw, Sbtw, wbtw_const_vadd_iff, (AddAction.injective v).ne_iff, (AddAction.injective v).ne_iff]

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