Theorems · Theorem · order theory

OrderIso.sumLexCongr_apply

∀ {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [inst : LE α₁] [inst_1 : LE α₂] [inst_2 : LE β₁]
  [inst_3 : LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) (a : α₁ ⊕ₗ β₁),
  (ea.sumLexCongr eb) a = toLex (Sum.map (⇑ea) (⇑eb) (ofLex a))

Defined in

Mathlib.Data.Sum.Order

Cited by

2 results in Mathlib

Foundations

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

Assumes

LELELELE