English
Let e1: α1 ≃o β1, e2: α2 ≃o β2, f1: β1 ≃o γ1, f2: β2 ≃o γ2 be order isomorphisms. Then the composition of the sum-congruences is compatible with composing the underlying isomorphisms, i.e. (e1.sumCongr e2).trans (f1.sumCongr f2) = (e1.trans f1).sumCongr (e2.trans f2).
Русский
Пусть e1: α1 ≃o β1, e2: α2 ≃o β2, f1: β1 ≃o γ1, f2: β2 ≃o γ2 — порядка-изomорфизмы. Тогда композиция конгруэнтностей по суммам совместима с композициями самих изоморфизмов: (e1.sumCongr e2).trans (f1.sumCongr f2) = (e1.trans f1).sumCongr (e2.trans f2).
LaTeX
$$$ (e_1 \mathrm{.sumCongr} e_2).\mathrm{trans} (f_1 \mathrm{.sumCongr} f_2) = (e_1 \mathrm{.trans} f_1).\mathrm{sumCongr} (e_2 \mathrm{.trans} f_2) $$$
Lean4
@[simp]
theorem sumCongr_trans (e₁ : α₁ ≃o β₁) (e₂ : α₂ ≃o β₂) (f₁ : β₁ ≃o γ₁) (f₂ : β₂ ≃o γ₂) :
(e₁.sumCongr e₂).trans (f₁.sumCongr f₂) = (e₁.trans f₁).sumCongr (e₂.trans f₂) := by ext; simp
