isIso_inl_of_epi_of_isColimit — Mathlib

English

If t is a colimit of f,f, then inl is an isomorphism.

Русский

Если t — колимит для (f,f), то inl — изоморфизм.

LaTeX

$$$\\text{isIso_inl_of_epi_of_isColimit }(t)$$$

Lean4

theorem isIso_inl_of_epi_of_isColimit {t : PushoutCocone f f} (ht : IsColimit t) : IsIso t.inl :=
  by
  refine ⟨⟨PushoutCocone.IsColimit.desc ht (𝟙 _) (𝟙 _) (by simp), by simp, ?_⟩⟩
  apply PushoutCocone.IsColimit.hom_ext ht
  · simp
  · simp [inl_eq_inr_of_epi_eq]

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