transfiniteCompositionsOfShape_eq_of_orderIso

English

If W is defined over a category C, then W.transfiniteCompositionsOfShape J equals W.transfiniteCompositionsOfShape J' whenever J and J' are order-isomorphic.

Русский

Для W над C равенство W.transfiniteCompositionsOfShape J и J' сохраняется при существовании порядка-изоморфизма между J и J'.

LaTeX

$$$W.transfiniteCompositionsOfShape J = W.transfiniteCompositionsOfShape J'$ when $J \\cong_o J'$$$

Lean4

theorem transfiniteCompositionsOfShape_eq_of_orderIso (e : J ≃o J') :
    W.transfiniteCompositionsOfShape J = W.transfiniteCompositionsOfShape J' :=
  by
  ext _ _ f
  exact ⟨fun ⟨h⟩ ↦ ⟨h.ofOrderIso e.symm⟩, fun ⟨h⟩ ↦ ⟨h.ofOrderIso e⟩⟩

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