arrow_mk_iso_iff — Mathlib

English

If Arrow.mk f and Arrow.mk g are isomorphic as arrows, then P f ⇔ P g for any morphism property P that respects isomorphisms.

Русский

Если стрелы Arrow.mk f и Arrow.mk g изоморфны как стрелы, то P f ⇔ P g для любого свойства P морфизмов, сохраняющего изоморфизмы.

LaTeX

$$$\\forall {W,X,Y,Z}\\ {f:W\\to X}\\{g:Y\\to Z},\\ (Arrow.mk\\,f)\\cong(Arrow.mk\\,g)\\Rightarrow P\\,f \\iff P\\,g.$$$

Lean4

theorem arrow_mk_iso_iff (P : MorphismProperty C) [RespectsIso P] {W X Y Z : C} {f : W ⟶ X} {g : Y ⟶ Z}
    (e : Arrow.mk f ≅ Arrow.mk g) : P f ↔ P g :=
  P.arrow_iso_iff e

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