English
Let ea1, ea2, eb1, eb2 be order isomorphisms. Then (ea1.sumLexCongr ea2).trans (eb1.sumLexCongr eb2) = (ea1.trans eb1).sumLexCongr (ea2.trans eb2).
Русский
Пусть ea1, ea2, eb1, eb2 — порядковые изоморфизмы. Тогда (ea1.sumLexCongr ea2).trans (eb1.sumLexCongr eb2) = (ea1.trans eb1).sumLexCongr (ea2.trans eb2).
LaTeX
$$$((ea_1.sumLexCongr ea_2).\mathrm{trans} (eb_1.sumLexCongr eb_2)) = ((ea_1.\mathrm{trans} eb_1).sumLexCongr (ea_2.\mathrm{trans} eb_2))$$$
Lean4
@[simp]
theorem sumLexCongr_trans (e₁ : α₁ ≃o β₁) (e₂ : α₂ ≃o β₂) (f₁ : β₁ ≃o γ₁) (f₂ : β₂ ≃o γ₂) :
(e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂) = (e₁.trans f₁).sumLexCongr (e₂.trans f₂) := by ext; simp
