wbtw_sub_const_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem wbtw_sub_const_iff {x y z : V} (v : V) : Wbtw R (x - v) (y - v) (z - v) ↔ Wbtw R x y z :=
  wbtw_vsub_const_iff v

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