isIso_inv_app — Mathlib

English

For α : F ⟶ G with IsIso α, the components of the inverse natural transformation satisfy (inv α).app X = inv (α.app X).

Русский

Для натурального преобразования α : F ⟶ G с условием IsIso α компоненты обратного преобразования удовлетворяют (inv α).app X = inv (α.app X).

LaTeX

$$$ (inv(\alpha)).app X = inv(\alpha.app X) $$$

Lean4

@[simp]
theorem isIso_inv_app (α : F ⟶ G) {_ : IsIso α} (X) : (inv α).app X = inv (α.app X) := by cat_disch

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