Theorems · Theorem · order theory

RelIso.sumLexComplLeft_apply

∀ {α : Type u_1} {r : α → α → Prop} {x : α} [inst : IsTrans α r] [inst_1 : Std.Trichotomous r] [inst_2 : DecidableRel r]
  (a : { x_1 // r x_1 x } ⊕ { x_1 // ¬r x_1 x }), (RelIso.sumLexComplLeft r x) a = (Equiv.sumCompl fun x_1 => r x_1 x) a

Defined in

Mathlib.Order.Hom.Lex

Cited by

0 results in Mathlib

Foundations

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

Assumes

IsTransStd.TrichotomousDecidableRel