English
If the union over U equals the whole domain, then f is injective iff each restriction to U_i is injective.
Русский
Если объединение по U равно всю область, то отображение f инъективно тогда и только тогда, когда каждое ограничение на U_i инъективно.
LaTeX
$$$\\text{Injective}(f) \\iff \\forall i,\\ \\text{Injective}((U(i)).\\text{restrictPreimage}(f)).$$$
Lean4
theorem injective_iff_injective_of_iUnion_eq_univ : Injective f ↔ ∀ i, Injective ((U i).restrictPreimage f) :=
by
refine ⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => ?_⟩
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (show f x ∈ Set.iUnion U by rw [hU]; trivial)
injection @H i ⟨x, hi⟩ ⟨y, show f y ∈ U i from e ▸ hi⟩ (Subtype.ext e)