mk'

Mathlib.Algebra.Homology.ShortComplex.ShortExact

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.ShortExact.mk'

English

Given an exact structure h on S and Mono S.f and Epi S.g, one can form the ShortExact structure.

Русский

Дано точное заполнение h на S и моно S.f и эпи S.g, можно построить ShortExact.

LaTeX

$$$ S.ShortExact $$$

Lean4

theorem mk' (h : S.Exact) (_ : Mono S.f) (_ : Epi S.g) : S.ShortExact where exact := h

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

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

Разделы

Аффилиация

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