bijective_iff_bijective_of_iUnion_eq_univ

English

If the union over U equals the universal set, then f is bijective iff every restriction to U_i is bijective.

Русский

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

LaTeX

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

Lean4

theorem bijective_iff_bijective_of_iUnion_eq_univ : Bijective f ↔ ∀ i, Bijective ((U i).restrictPreimage f) :=
  by
  rw [Bijective, injective_iff_injective_of_iUnion_eq_univ hU, surjective_iff_surjective_of_iUnion_eq_univ hU]
  simp [Bijective, forall_and]

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