inv_snd

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

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

← MathLib Explorer

English

The snd component of the inverse morphism coincides with the inverse of snd.

Русский

Компонента snd в обратном морфизме совпадает с обратной компонентой snd.

LaTeX

$$$ (inv f).snd = inv (f.snd) $$$

Lean4

@[simp]
theorem inv_snd : (inv f).snd = inv f.snd := by
  symm
  apply IsIso.inv_eq_of_hom_inv_id
  simpa [-IsIso.hom_inv_id] using congrArg (fun t ↦ t.snd) (IsIso.hom_inv_id f)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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