instPreregular — Mathlib

English

The category CompHaus is preregular, i.e., certain factorization properties hold for epis and surjections.

Русский

Категория CompHaus является прегрегулярной, то есть выполняются определенные факторизации для эпиморфизмов и сюръективных отображений.

LaTeX

$$$\mathbf{Preregular}(\mathbf{CompHaus})$$$

Lean4

instance : Preregular CompHaus :=
  preregular fun _ _ _ ↦ ((effectiveEpi_tfae _).out 0 2).mp

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