instIsIsoT

Mathlib.Topology.Gluing

URI: https://scilib.ai/kg/mathlib#TopCat.GlueData.instIsIsoT

English

For any MkCore h and indices i, j, the transition map t_{i j} is an isomorphism.

Русский

Для любого h и индексов i, j переходное отображение t_{i j} является изоморфизмом.

LaTeX

$$For all h, i, j, h.t_{i j} is an isomorphism.$$

Lean4

instance (h : MkCore.{u}) (i j : h.J) : IsIso (h.t i j) := by use h.t j i; constructor <;> ext1;
  exacts [h.t_inv _ _ _, h.t_inv _ _ _]

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

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

Разделы

Аффилиация

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