map_bijective — Mathlib

English

Bijectivity of PLift.map f is equivalent to bijectivity of f.

Русский

Биективность отображения PLift.map f эквивалентна биективности f.

LaTeX

$$$\\forall {\\alpha \\beta} {f : \\alpha \\rightarrow \\beta}, \\operatorname{Bijective}(\\mathrm{PLift.map} f) \\Leftrightarrow \\operatorname{Bijective}(f)$$$

Lean4

@[simp]
theorem map_bijective : Bijective (PLift.map f) ↔ Bijective f :=
  (down_bijective.of_comp_iff _).trans <| Bijective.of_comp_iff' up_bijective _

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