Commit 2026-01-30 17:31 33259589

View on Github →

feat(Order): order types (#34034) Adding the basic definitions around order types, the equivalence classes of linear orders under order isomorphism.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Category/LinOrd.lean

deleted structure LinOrd

Modified Mathlib/Order/Defs/LinearOrder.lean

added structure LinOrd

Created Mathlib/Order/Types/Defs.lean

added def OrderType.ToType

added theorem OrderType.bot_eq_zero

added theorem OrderType.inductionOn

added theorem OrderType.inductionOn₂

added theorem OrderType.inductionOn₃

added def OrderType.instSetoid

added def OrderType.liftOn

added theorem OrderType.liftOn_type

added def OrderType.omega0

added theorem OrderType.pos_iff_ne_zero

added def OrderType.type

added theorem OrderType.type_congr

added theorem OrderType.type_eq_one

added theorem OrderType.type_eq_type

added theorem OrderType.type_eq_zero

added theorem OrderType.type_le_type

added theorem OrderType.type_le_type_iff

added theorem OrderType.type_lt_type

added theorem OrderType.type_nat

added theorem OrderType.type_ne_zero

added theorem OrderType.type_ne_zero_iff

added theorem OrderType.type_of_isEmpty

added theorem OrderType.type_of_unique

added theorem OrderType.type_toType

added def OrderType