diagramIso_inv_app_left

Mathlib.CategoryTheory.GlueData

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GlueData.diagramIso_inv_app_left

English

The inverse component of the diagram isomorphism at the left entry is the identity.

Русский

Обратный компонент изоморфизма диаграмм на левой позиции является тождественным.

LaTeX

$$$(D.diagramIso F).inv.app(\\text{WalkingMultispan.left}) = \\mathrm{Id}$$$

Lean4

@[simp]
theorem diagramIso_inv_app_left (i : D.J × D.J) : (D.diagramIso F).inv.app (WalkingMultispan.left i) = 𝟙 _ :=
  rfl

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

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

Разделы

Аффилиация

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