Theorems · Definition · order theory

OrderIso.sumLexIicIoi

{α : Type u_1} → [inst : LinearOrder α] → (x : α) → ↑(Set.Iic x) ⊕ₗ ↑(Set.Ioi x) ≃o α

A linear order is isomorphic to the lexicographic sum of elements less or equal to x and elements greater than x.

Defined in

Mathlib.Order.Hom.Lex

Cited by

6 results in Mathlib

Foundations

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

Assumes

LinearOrder