Theorems · Definition · order theory

OrderIso.sumLexCongr

{α₁ : Type u_4} →
  {α₂ : Type u_5} →
    {β₁ : Type u_6} →
      {β₂ : Type u_7} →
        [inst : LE α₁] →
          [inst_1 : LE α₂] → [inst_2 : LE β₁] → [inst_3 : LE β₂] → α₁ ≃o α₂ → β₁ ≃o β₂ → α₁ ⊕ₗ β₁ ≃o α₂ ⊕ₗ β₂

Equiv.sumCongr promoted to an order isomorphism between lexicographic sums.

Defined in

Mathlib.Data.Sum.Order

Cited by

4 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound

Assumes

LELELELE