Theorems · Inductive type · order theory
LinearOrder
Type u_2 → Type u_2
A linear order is reflexive, transitive, antisymmetric and total relation ≤.
We assume that every linear ordered type has decidable (≤), (<), and (=).
- Defined in
- Mathlib.Order.Defs.LinearOrder
- Cited by
- 8,572 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by9,368
Results whose statement or proof uses this declaration.
- le_of_not_gtstatement and proof · cited by 430
- FloorRingstatement · cited by 405
- lt_of_not_gestatement and proof · cited by 374
- not_lestatement and proof · cited by 328
- not_ltstatement and proof · cited by 306
- le_totalstatement and proof · cited by 294
- le_or_gtstatement and proof · cited by 269
- ArchimedeanClassstatement and proof · cited by 247
- Int.floorstatement and proof · cited by 225
- le_max_leftstatement and proof · cited by 215
- le_max_rightstatement and proof · cited by 205
- CauSeqstatement and proof · cited by 189
Showing the 200 most cited of 9,368.