comp_isIso' — Mathlib

English

If f and h are isomorphisms, then their composition f ≫ h is an isomorphism.

Русский

Если f и h — изоморфизмы, то их композиция f ≫ h также является изоморфизмом.

LaTeX

$$$IsIso\ f\to IsIso\ h\to IsIso\ (f\gg h)$$$

Lean4

/-- The composition of isomorphisms is an isomorphism. Here the arguments of type `IsIso` are
explicit, to make this easier to use with the `refine` tactic, for instance.
-/
theorem comp_isIso' (_ : IsIso f) (_ : IsIso h) : IsIso (f ≫ h) :=
  inferInstance

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