Theorems · Definition · order theory

RelIso.sumLexComplRight

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

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

Defined in

Mathlib.Order.Hom.Lex

Cited by

2 results in Mathlib

Foundations

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

Assumes

IsTransStd.TrichotomousDecidableRel