English
Equiv.sumCongr promoted to an order isomorphism between lexicographic sums: sumLexCongr (ea : α1 ≃o α2) (eb : β1 ≃o β2) : α1 ⊕ₗ β1 ≃o α2 ⊕ₗ β2.
Русский
Equiv.sumCongr преобразуется в порядок-изоморфизм между лексикографическими суммами: sumLexCongr (ea) (eb) : α1 ⊕ₗ β1 ≃o α2 ⊕ₗ β2.
LaTeX
$$$\text{sumLexCongr }(e_a,e_b) : \alpha_1 \oplus_{\mathrm{lex}} \beta_1 \cong_o \alpha_2 \oplus_{\mathrm{lex}} \beta_2$$$
Lean4
/-- `Equiv.sumCongr` promoted to an order isomorphism between lexicographic sums. -/
@[simps! apply]
def sumLexCongr (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) : α₁ ⊕ₗ β₁ ≃o α₂ ⊕ₗ β₂
where
toEquiv := ofLex.trans ((Equiv.sumCongr ea eb).trans toLex)
map_rel_iff' := by simp_rw [Lex.forall]; rintro (a | a) (b | b) <;> simp
