instIsIsoWhiskerLeft

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.CatCospanTransform.instIsIsoWhiskerLeft

English

There is an instance providing that whiskering a morphism on the left by an isomorphism yields an isomorphism.

Русский

Существует инстанс, что взвешивание на левой стороне морфизма по изоморфизму даёт изоморфизм.

LaTeX

$$IsIso (ψ ◁ θ)$$

Lean4

instance : IsIso (ψ ◁ θ) :=
  ⟨ψ ◁ inv θ, ⟨by simp [← whiskerLeft_comp], by simp [← whiskerLeft_comp]⟩⟩

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

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

Разделы

Аффилиация

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