wbtw_map_iff — Mathlib

English

Under an affine map f, Wbtw x y z holds for the image if and only if it holds for the original: Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z, given f is injective.

Русский

При аффинном отображении f равенство Wbtw сохраняется и обратно: Wbtw R (f x) (f y) (f z) ⇔ Wbtw R x y z, при условии инъективности f.

LaTeX

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

Lean4

theorem wbtw_map_iff {x y z : P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z :=
  by
  refine ⟨fun h => ?_, fun h => h.map _⟩
  rwa [Wbtw, ← affineSegment_image, hf.mem_set_image] at h

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