injective_iff_injective_of_iUnion_eq_univ

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)

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