instMonoF'

Mathlib.CategoryTheory.GlueData

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instMonoF'

English

For glue data D and indices i, j, the glue maps f' i j are monomorphisms.

Русский

Для данных склейки D и индексов i, j отображения f' i j мононозы (моно-морфизмы).

LaTeX

$$$\forall i,j:\, D.J,\; Mono\,(D.f' i j)$$$

Lean4

instance (D : GlueData' C) (i j : D.J) : Mono (D.f' i j) := by dsimp [GlueData'.f']; split_ifs <;> infer_instance

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

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

Разделы

Аффилиация

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