wbtw_map_iff — Mathlib

English

The Wbtw property is preserved under an affine equivalence: Wbtw R x y z holds if and only if Wbtw R (f x) (f y) (f z) for an affine equivalence f.

Русский

Свойство Wbtw сохраняется при аффинном эквивалентном отображении: Wbtw R x y z сохраняется тогда и только тогда при Wbtw R (f x) (f y) (f z) для аффинного эквивалента f.

LaTeX

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

Lean4

@[simp]
theorem wbtw_map_iff {x y z : P} (f : P ≃ᵃ[R] P') : Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z :=
  by
  have : Function.Injective f.toAffineMap := f.injective
  apply this.wbtw_map_iff

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