map_bijective — Mathlib

English

For any f : α → β, ULift.map f is bijective if and only if f is bijective.

Русский

Для любого f : α → β ULift.map f биективно тогда и только тогда, когда f биективен.

LaTeX

$$$\\operatorname{Bijective}(\\mathrm{ULift.map}\,f) \\iff \\operatorname{Bijective}(f)$$$

Lean4

@[simp]
theorem map_bijective : Bijective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Bijective f :=
  (down_bijective.of_comp_iff _).trans <| Bijective.of_comp_iff' up_bijective _

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