Theorems · Theorem · order theory

RelIso.emptySumLex_apply

∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsEmpty α] (a : α ⊕ β),
  (RelIso.emptySumLex r s) a = (Equiv.sumEmpty β α) a.swap

Defined in

Mathlib.Order.RelIso.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

IsEmpty