isIso_of_isIso_apply — Mathlib

English

If a morphism f between graded objects is componentwise an isomorphism, then f is an isomorphism.

Русский

Если морфизм f между градуированными объектами компонентно является изоморфизмом, то f — изоморфизм.

LaTeX

$$$ \\forall i, IsIso (f i) \\Rightarrow IsIso f $$$

Lean4

theorem isIso_of_isIso_apply (f : X ⟶ Y) [hf : ∀ i, IsIso (f i)] : IsIso f :=
  by
  change IsIso (isoMk X Y (fun i => asIso (f i))).hom
  infer_instance

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