sbtw_map_iff — Mathlib

English

For an affine equivalence f, Sbtw R x y z holds if and only if Sbtw R (f x) (f y) (f z) holds.

Русский

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

LaTeX

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

Lean4

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

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