instEpiFNatπ — Mathlib

English

For every natural number n, the morphism P.π.f n is an epimorphism. The base case n = 0 follows from the colimit property; for successors, it follows from π_f_succ.

Русский

Для каждого натурального числа n отображение P.π.f n является эпиморфизмом. Базовый случай n = 0 следует из свойств колимита; для перехода к следующему случаю следует из π_f_succ.

LaTeX

$$$\forall n,\; Epi\bigl(P.\pi.f\,n\bigr)$$$

Lean4

instance (n : ℕ) : Epi (P.π.f n) := by
  cases n
  · exact epi_of_isColimit_cofork P.isColimitCokernelCofork
  · rw [π_f_succ]; infer_instance

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