isIso_app_of_isIso — Mathlib

English

The components of a natural transformation that is an isomorphism form isomorphisms: if α : F ⟶ G and α is an isomorphism, then for every X, α.app X is an isomorphism.

Русский

Компоненты натурального преобразования, являющегося изоморфизмом, самИ являются изоморфизмами: если α : F ⟶ G и α является изоморфизмом, то для каждого X компонентα_X является изоморфизмом.

LaTeX

$$$ IsIso(\alpha_{X}) \quad \text{for all } X $$$

Lean4

/-- The components of a natural isomorphism are isomorphisms.
-/
instance isIso_app_of_isIso (α : F ⟶ G) [IsIso α] (X) : IsIso (α.app X) :=
  ⟨⟨(inv α).app X, ⟨by grind, by grind⟩⟩⟩

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