instRespectsIsoTransfiniteCompositionsOfShape

English

The construction W.transfiniteCompositionsOfShape J respects isomorphisms of arrows: if an arrow e is an isomorphism, then mapping along e preserves membership in the transfinite composition property.

Русский

Конструкция W.transfiniteCompositionsOfShape J сохраняет изоморфизмы стрел: если стрелка является изоморфизмом, отображение по ней сохраняет принадлежность к свойству трансфинитной композиции.

LaTeX

$$$\\text{RespectsIso}(W.TransfiniteCompositionOfShape J)$, i.e., isomorphisms preserve transfinite compositions$$

Lean4

instance : RespectsIso (W.transfiniteCompositionsOfShape J) :=
  RespectsIso.of_respects_arrow_iso _ (fun _ _ e ⟨h⟩ ↦ ⟨h.ofArrowIso e⟩)

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