iff_of_arrow_iso — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall A,B,A',B',\\; (e:\\mathrm{Iso}(\\mathrm{Arrow}(f),\\mathrm{Arrow}(g)))\\;\\Rightarrow\\; (\\mathrm{StrongMono}(f) \\iff \\mathrm{StrongMono}(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) :
    StrongMono f ↔ StrongMono g := by
  constructor <;> intro
  exacts [StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm]

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