isIso — Mathlib

English

If a morphism f is the endpoint of a transfinite composition of shape J where every stage is an isomorphism, then f itself is an isomorphism.

Русский

Если морфизм f является концом трансфинитной композиции формы J, все звенья которой изоморфизмы, то и сам f — изоморфизм.

LaTeX

$$$ \text{If } h : (\text{isomorphisms } C).TransfiniteCompositionOfShape\ J\ f,\ \ \text{then } f \text{ isIso}.$$

Lean4

theorem isIso : IsIso f :=
  (isomorphisms C).transfiniteCompositionsOfShape_le _ _ h.mem

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