map_surjective — Mathlib

English

For any f : α → β, the surjectivity of ULift.map f is equivalent to the surjectivity of f.

Русский

Для любого f : α → β сюръективность ULift.map f эквивалентна сюръективности f.

LaTeX

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

Lean4

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

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