surjective_iff_surjective_of_iUnion_eq_univ

English

If the union over U equals the whole domain, then f is surjective iff each restriction to U_i is surjective.

Русский

Если объединение по U равно всю область, то отображение f сюръективно тогда и только тогда, когда каждое ограничение на U_i сюръективно.

LaTeX

$$$\\text{Surjective}(f) \\iff \\forall i,\\ \\text{Surjective}((U(i)).\\text{restrictPreimage}(f)).$$$

Lean4

theorem surjective_iff_surjective_of_iUnion_eq_univ : Surjective f ↔ ∀ i, Surjective ((U i).restrictPreimage f) :=
  by
  refine ⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => ?_⟩
  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (show x ∈ Set.iUnion U by rw [hU]; trivial)
  exact ⟨_, congr_arg Subtype.val (H i ⟨x, hi⟩).choose_spec⟩

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