isIso_of_isIso_app — Mathlib

English

A natural transformation is an isomorphism if all its components are isomorphisms.

Русский

Натуральное преобразование является изоморфизмом, если все его компоненты являются изоморфизмами.

LaTeX

$$$ \forall X, IsIso(\alpha_{X}) \Rightarrow IsIso(\alpha) $$$

Lean4

/-- A natural transformation is an isomorphism if all its components are isomorphisms.
-/
theorem isIso_of_isIso_app (α : F ⟶ G) [∀ X : C, IsIso (α.app X)] : IsIso α :=
  (ofComponents (fun X => asIso (α.app X)) (by simp)).isIso_hom

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