instIsIsoMapF

Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.instIsIsoMapF

English

For every morphism f in the indexing category, the image under h.F.map f is an isomorphism.

Русский

Для каждого морфизма f в индексационной категории образ h.F.map f является изоморфизмом.

LaTeX

$$$ \forall i,j:\, (i\to j),\ IsIso(h.F.map(i\to j)).$$

Lean4

instance {i j : J} (f : i ⟶ j) : IsIso (h.F.map f) :=
  h.mem_map f

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

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

Разделы

Аффилиация

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