map_bijective — Mathlib

English

Surjective (Prod.map f g) is equivalent to Surjective f and Surjective g under Nonempty assumptions.

Русский

Сюръективность Prod.map эквивалентна сюръективности каждой функции f и g при некоторых предположениях о непустоте.

LaTeX

$$Iff (Surjective (Prod.map f g)) (And (Surjective f) (Surjective g))$$

Lean4

@[simp]
theorem map_bijective [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :
    Bijective (map f g) ↔ Bijective f ∧ Bijective g :=
  by
  haveI := Nonempty.map f ‹_›
  haveI := Nonempty.map g ‹_›
  exact (map_injective.and map_surjective).trans and_and_and_comm

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