instHasTwoOutOfThreePropertyIsomorphisms

English

For any category C, the class of isomorphisms is stable under the two-out-of-three principle: if two of f, g, and f∘g are isomorphisms, then the third is as well.

Русский

Для любой категории C множество изоморфизмов удовлетворяет принципу двух из трёх: если две из трёх величин f, g и f∘g являются изоморфизмами, то третья также является изоморфизмом.

LaTeX

$$$\\text{Isomorphisms}(C) \\text{ is two-out-of-three under composition: if } f,g,\\; f\\circ g \\text{ are isomorphisms then the remaining one is as well.}$$$

Lean4

instance : (isomorphisms C).HasTwoOutOfThreeProperty
    where
  of_postcomp f
    g := fun (hg : IsIso g) (hfg : IsIso (f ≫ g)) => by simpa using (inferInstance : IsIso ((f ≫ g) ≫ inv g))
  of_precomp f g := fun (hf : IsIso f) (hfg : IsIso (f ≫ g)) => by simpa using (inferInstance : IsIso (inv f ≫ (f ≫ g)))

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