Theorems · Definition · order theory

OrderIso.sumLexIioIci

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

A linear order is isomorphic to the lexicographic sum of elements less than x and elements greater or equal to 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