ofArrowIso — Mathlib

English

If f is a transfinite composition of shape J in W and J' is order-isomorphic to J, then f is a transfinite composition of shape J' in W.

Русский

Если f является трансфинитной композицией формы J в W и J' имеет биективное соответствие порядка с J, тогда f является трансфинитной композицией формы J' в W.

LaTeX

$$$\text{If } h: W.TransfiniteCompositionOfShape J f \text{ and } e : J' \simeq_o J, \; W.TransfiniteCompositionOfShape J' f$$$

Lean4

/-- If `f` and `f'` are two isomorphic morphisms and `f` is a transfinite composition
of morphisms in `W : MorphismProperty C`, then so is `f'`. -/
@[simps toTransfiniteCompositionOfShape]
def ofArrowIso {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : W.TransfiniteCompositionOfShape J f'
    where
  __ := h.toTransfiniteCompositionOfShape.ofArrowIso e
  map_mem := h.map_mem

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