instIsIsoF'

Mathlib.CategoryTheory.GlueData

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

English

For every index i, the morphism f' i i is an isomorphism.

Русский

Для каждого i мономорфизм f' i i является изоморфизмом.

LaTeX

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

Lean4

instance (D : GlueData' C) (i : D.J) : IsIso (D.f' i i) := by simp only [GlueData'.f', ↓reduceDIte]; infer_instance

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

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

Разделы

Аффилиация

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