instMonoFTruncLE'ToRestriction

Mathlib.Algebra.Homology.Embedding.TruncLE

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instMonoFTruncLE'ToRestriction

English

There is a mono structure on each component (K.truncLE'ToRestriction e).f i.

Русский

У каждого компонента (K.truncLE'ToRestriction e).f i есть монообразование.

LaTeX

$$$\text{Mono}\bigl((K.truncLE'ToRestriction e).f i\bigr)$$$

Lean4

instance (i : ι) : Mono ((K.truncLE'ToRestriction e).f i) :=
  inferInstanceAs (Mono ((K.op.restrictionToTruncGE' e.op).f i).unop)

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

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

Разделы

Аффилиация

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