EffectiveEpi

Mathlib.CategoryTheory.EffectiveEpi.Comp

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

English

If f is a split epi, then f is an effective epi.

Русский

Если f является разложимой эпиморфией, то она эффективна.

LaTeX

$$$\operatorname{IsSplitEpi}(f) \Rightarrow \operatorname{EffectiveEpi}(f)$$$

Lean4

instance EffectiveEpi {B X : C} (f : X ⟶ B) [IsSplitEpi f] : EffectiveEpi f :=
  by
  rw [← Category.comp_id f]
  infer_instance

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

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

Разделы

Аффилиация

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