instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso

English

If W respects iso then the costructured arrow object is closed under isomorphisms.

Русский

Если W сохраняет изоморфизмы, то объект CostructuredArrow замкнут относительно изоморфизмов.

LaTeX

$$$\\text{IsClosedUnderIsomorphisms}(W.costructuredArrowObj L (X := X))$$$

Lean4

instance [W.RespectsIso] : (W.costructuredArrowObj L (X := X)).IsClosedUnderIsomorphisms :=
  inferInstanceAs <| (W.commaObj _ _).IsClosedUnderIsomorphisms

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