Theorems · Definition · order theory

RelIso.sumLexCongr

{α₁ : Type u_5} →
  {α₂ : Type u_6} →
    {β₁ : Type u_7} →
      {β₂ : Type u_8} →
        {r₁ : α₁ → α₁ → Prop} →
          {r₂ : α₂ → α₂ → Prop} →
            {s₁ : β₁ → β₁ → Prop} → {s₂ : β₂ → β₂ → Prop} → r₁ ≃r s₁ → r₂ ≃r s₂ → Sum.Lex r₁ r₂ ≃r Sum.Lex s₁ s₂

Given relation isomorphisms r₁ ≃r s₁ and r₂ ≃r s₂, construct a relation isomorphism for the lexicographic orders on the sum.

Defined in

Mathlib.Order.RelIso.Basic

Cited by

2 results in Mathlib

Foundations

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