instIsIsoFst

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.CategoricalPullback.instIsIsoFst

English

If f is an isomorphism in the categorical pullback, then its fst component is an isomorphism.

Русский

Если f — изоморфизм в категориальномpullback, то его компонент fst тоже изоморфизм.

LaTeX

$$$ IsIso\ f \Rightarrow IsIso\ f.fst$$$

Lean4

instance : IsIso f.fst :=
  inferInstanceAs (IsIso ((π₁ _ _).mapIso (asIso f)).hom)

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

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

Разделы

Аффилиация

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