ofOrderIso — Mathlib

English

There is a construction that transports a transfinite composition along an order-iso J' ≃o J, producing a transfinite composition of shape J' in W.

Русский

Существует построение, переносящее трансфинитную композицию вдоль порядка-изоморфизма J' ≃o J, порождающее трансфинитную композицию формы J' в W.

LaTeX

$$$\text{ofOrderIso} : W.TransfiniteCompositionOfShape J f \to W.TransfiniteCompositionOfShape J' f \text{ given } e : J' \simeq_o J$$$

Lean4

/-- If `f` is a transfinite composition of shape `J` of morphisms in `W`,
then it is also a transfinite composition of shape `J'` of morphisms in `W` if `J' ≃o J`. -/
def ofOrderIso {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) :
    W.TransfiniteCompositionOfShape J' f
    where
  __ := h.toTransfiniteCompositionOfShape.ofOrderIso e
  map_mem j
    hj := by
    have := h.map_mem (e j) (by simpa only [e.isMax_apply])
    rw [← W.arrow_mk_mem_toSet_iff] at this ⊢
    have eq : Arrow.mk (homOfLE (e.monotone (Order.le_succ j))) = Arrow.mk (homOfLE (Order.le_succ (e j))) :=
      Arrow.ext rfl (e.map_succ j) rfl
    replace eq := congr_arg h.F.mapArrow.obj eq
    convert this using 1

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