epi

Mathlib.CategoryTheory.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsSplitEpi.epi

English

Every split epi is an epi.

Русский

Любой раздельный эпиморфизм является эпиморфизмом.

LaTeX

$$$ \forall X,Y\,(f: X \to Y),\; \mathrm{SplitEpi}(f) \Rightarrow \mathrm{Epi}(f).$$$

Lean4

/-- Every split epi is an epi. -/
instance (priority := 100) epi {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : Epi f :=
  hf.exists_splitEpi.some.epi

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru