Theorems · Definition · order theory

RelIso.sumLexComplLeft

{α : Type u_1} →
  (r : α → α → Prop) →
    (x : α) →
      [IsTrans α r] →
        [Std.Trichotomous r] →
          [DecidableRel r] → Sum.Lex (Subrel r fun x_1 => r x_1 x) (Subrel r fun x_1 => ¬r x_1 x) ≃r r

A relation is isomorphic to the lexicographic sum of elements less than x and elements not less than x.

Defined in

Mathlib.Order.Hom.Lex

Cited by

3 results in Mathlib

Foundations

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

Assumes

IsTransStd.TrichotomousDecidableRel