isIso_limit_cone_parallelPair_of_eq

English

If f = g, then any limit fork c for (f,g) has c.ι an isomorphism.

Русский

Если f = g, то любой предел-форк c для (f,g) имеет c.ι является изоморфизмом.

LaTeX

$$$(f = g) \Rightarrow \forall c:\, \mathrm{Fork}(f,g), \mathrm{IsLimit}(c) \Rightarrow \mathrm{IsIso}(c.\iota)$$$

Lean4

/-- Every equalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
theorem isIso_limit_cone_parallelPair_of_eq (h₀ : f = g) {c : Fork f g} (h : IsLimit c) : IsIso c.ι :=
  Iso.isIso_hom <| IsLimit.conePointUniqueUpToIso h <| isLimitIdFork h₀

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