sbtw_map_iff — Mathlib

English

If f is injective, then Wbtw R (f x) (f y) (f z) holds if and only if Wbtw R x y z holds.

Русский

Если f инъективно, то Wbtw R (f x) (f y) (f z) выполняется тогда и только тогда, когда Wbtw R x y z выполняется.

LaTeX

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

Lean4

theorem sbtw_map_iff {x y z : P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z := by simp_rw [Sbtw, hf.wbtw_map_iff, hf.ne_iff]

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