map — Mathlib

English

Wbtw is preserved under affine maps: if x, y, z are in P with Wbtw R x y z, and f is an affine map P →ᵃ[R] P', then Wbtw R (f x) (f y) (f z).

Русский

Wbtw сохраняется под аффинными отображениями: если x, y, z удовлетворяют Wbtw R x y z и f : P →ᵃ[R] P', то Wbtw R (f x) (f y) (f z).

LaTeX

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

Lean4

theorem map {x y z : P} (h : Wbtw R x y z) (f : P →ᵃ[R] P') : Wbtw R (f x) (f y) (f z) :=
  by
  rw [Wbtw, ← affineSegment_image]
  exact Set.mem_image_of_mem _ h

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