instHasOfPostcompPropertyIsomorphismsOfRespectsIso

English

If W has the Isomorphisms structure and W is stable under postcomposition, then W.HasOfPostcompProperty is inherited by isomorphisms.

Русский

Если W удовлетворяет свойству Изоморфизмов и устойчиво к посткомпозиции, то Isomorphisms сохраняют свойство HasOfPostcompProperty.

LaTeX

$$$ [W.\\text{RespectsIso}] \\Rightarrow W.HasOfPostcompProperty (\\text{isomorphisms } C).$$$

Lean4

instance [W.RespectsIso] : W.HasOfPostcompProperty (isomorphisms C) where
  of_postcomp _ _ (_ : IsIso _) := (W.cancel_right_of_respectsIso _ _).mp

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