isIso_limit_cone_parallelPair_of_epi

English

If t is a fork of f,g and Fork.ι t is epi, then f = g.

Русский

Если t — форк f,g и Fork.ι t эпиморфизм, то f = g.

LaTeX

$$$t:\mathrm{Fork}(f,g)\; \&\&\ \mathrm{Epi}(\mathrm{Fork.} \iota t)\Rightarrow f = g$$$

Lean4

/-- An equalizer that is an epimorphism is an isomorphism. -/
theorem isIso_limit_cone_parallelPair_of_epi {c : Fork f g} (h : IsLimit c) [Epi c.ι] : IsIso c.ι :=
  isIso_limit_cone_parallelPair_of_eq ((cancel_epi _).1 (Fork.condition c)) h

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