epi_iff_surjective — Mathlib

English

In PresheafOfModules, a morphism f is epi if and only if each f.app X is surjective.

Русский

В PresheafOfModules стрелка f является эпиморфизмом тогда и только тогда, когда каждый f.app X сюръективен.

LaTeX

$$Epi f ↔ ∀ X, Function.Surjective (f.app X)$$

Lean4

theorem epi_iff_surjective : Epi f ↔ ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective (f.app X) :=
  ⟨fun _ ↦ surjective_of_epi f, epi_of_surjective⟩

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