iff_of_arrow_iso — Mathlib

English

If there is an isomorphism between arrows e: Arrow f ≅ Arrow g, then StrongEpi f holds iff StrongEpi g holds.

Русский

Если между стрелами f и g существует изоморфизм стрел e: Arrow f ≅ Arrow g, тогда StrongEpi f эквивалentно StrongEpi g.

LaTeX

$$$\\forall A,B,A',B',\\; (e:\\mathrm{Iso}(\\mathrm{Arrow}(f),\\mathrm{Arrow}(g)))\\;\\Rightarrow\\; (\\mathrm{StrongEpi}(f) \\iff \\mathrm{StrongEpi}(g)).$$$

Lean4

theorem iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : Arrow.mk f ≅ Arrow.mk g) :
    StrongEpi f ↔ StrongEpi g := by
  constructor <;> intro
  exacts [StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm]

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