of_vert_isIso_epi — Mathlib

English

If g is an epimorphism and inl is an isomorphism, for a commutative square, the square is a pushout: IsPushout f g inl inr.

Русский

Если g — эпиморфизм и inl — изоморфизм, для коммутивной схемы пуш-аут равен: IsPushout f g inl inr.

LaTeX

$$$ [\\operatorname{Epi}\\ g] \\ [\\operatorname{IsIso} inl] (\\text{sq} : \\operatorname{CommSq} f g inl inr) \\Rightarrow \\operatorname{IsPushout} f g inl inr $$$

Lean4

theorem of_vert_isIso_epi [Epi g] [IsIso inl] (sq : CommSq f g inl inr) : IsPushout f g inl inr :=
  (of_horiz_isIso_epi sq.flip).flip

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