English
Promote a pair of order isomorphisms between α₁ ≃o α₂ and β₁ ≃o β₂ to an order isomorphism between the lexicographic sums α₁ ⊕ₗ β₁ and α₂ ⊕ₗ β₂; this is realized by a functorial construction SumCongr.
Русский
Преобразование пары порядочных изоморфизмов между α₁ ≃o α₂ и β₁ ≃o β₂ в порядок-изоморфизм между лексикографическими суммами α₁ ⊕ₗ β₁ и α₂ ⊕ₗ β₂; реализуется через SumCongr.
LaTeX
$$$\\text{sumCongr} : (\\alpha_1 \\simeq_o \\alpha_2) \\to (\\beta_1 \\simeq_o \\beta_2) \\to (\\alpha_1 \\oplus β_1) \\simeq_o (\\alpha_2 \\oplus β_2)$$$
Lean4
/-- `Equiv.sumCongr` promoted to an order isomorphism. -/
@[simps! apply]
def sumCongr (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) : α₁ ⊕ β₁ ≃o α₂ ⊕ β₂
where
toEquiv := .sumCongr ea eb
map_rel_iff' := by aesop
