instMonoιTruncLE

Mathlib.Algebra.Homology.Embedding.TruncLE

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instMonoιTruncLE

English

The morphism K.ιTruncLE e is a monomorphism in the ambient category of HomologicalComplex.

Русский

Морфизм K.ιTruncLE e является моно в окружении HomologicalComplex.

LaTeX

$$$ \text{Mono}\big( K.ιTruncLE e \big)$$$

Lean4

instance : Mono (K.ιTruncLE e) :=
  mono_of_mono_f _ (fun _ => inferInstance)

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

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

Разделы

Аффилиация

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