isIso_fst_of_mono_of_isLimit — Mathlib

English

Let t be a pullback cone of f with f and ht be a limit; if f is mono, then t.snd is an isomorphism.

Русский

Пусть t — pullback-конус для f, ht — предел, и f моно. Тогда t.snd — изоморфизм.

LaTeX

$$$IsIso\ t.snd$$$

Lean4

theorem isIso_fst_of_mono_of_isLimit {t : PullbackCone f f} (ht : IsLimit t) : IsIso t.fst :=
  by
  refine ⟨⟨PullbackCone.IsLimit.lift ht (𝟙 _) (𝟙 _) (by simp), ?_, by simp⟩⟩
  apply PullbackCone.IsLimit.hom_ext ht
  · simp
  · simp [fst_eq_snd_of_mono_eq]

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