English
Let e1: α ≃o β and e2: β ≃o γ be order isomorphisms. The top-extension construction e ↦ e.withTopCongr is compatible with composition, i.e. the top-extension of the composite equals the composite of the top-extensions.
Русский
Пусть e1: α ≃o β и e2: β ≃o γ — это упорядоченные изоморфизмы. При возведении к верхнему элементу (top-extension) композиция сохраняется: верхнее расширение композиции равно композиции верхних расширений.
LaTeX
$$$ (e_1 \text{ trans } e_2)^{\mathrm{withTopCongr}} = e_1^{\mathrm{withTopCongr}} \text{ trans } e_2^{\mathrm{withTopCongr}} $$$
Lean4
@[simp]
theorem withTopCongr_trans (e₁ : α ≃o β) (e₂ : β ≃o γ) :
(e₁.trans e₂).withTopCongr = e₁.withTopCongr.trans e₂.withTopCongr :=
RelIso.toEquiv_injective <| e₁.toEquiv.withTopCongr_trans e₂.toEquiv
