wbtw_vsub_const_iff — Mathlib

English

Under an injective affine map f, Sbtw R (f x) (f y) (f z) holds iff Sbtw R x y z holds.

Русский

При инъективном аффинном отображении f выполняется эквивалентность: Sbtw R (f x) (f y) (f z) ⇔ Sbtw R x y z.

LaTeX

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

Lean4

@[simp]
theorem wbtw_vsub_const_iff {x y z : P} (p : P) : Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Wbtw R x y z :=
  mem_vsub_const_affineSegment _

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