Theorems · Inductive type · order theory
PartialOrder
Type u_2 → Type u_2
A partial order is a reflexive, transitive, antisymmetric relation ≤.
- Defined in
- Mathlib.Order.Defs.PartialOrder
- Cited by
- 6,410 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 by7,194
Results whose statement or proof uses this declaration.
- IsStrictOrderedRingstatement · cited by 2,490
- Disjointstatement and proof · cited by 2,201
- le_antisymmstatement and proof · cited by 2,068
- IsOrderedRingstatement · cited by 777
- Archimedeanstatement · cited by 603
- zero_lt_onestatement and proof · cited by 598
- StarOrderedRingstatement · cited by 587
- Convexstatement and proof · cited by 551
- HahnSeriesstatement · cited by 528
- LE.le.antisymmstatement · cited by 507
- AbsoluteValuestatement · cited by 363
- Orientationstatement and proof · cited by 360
Showing the 200 most cited of 7,194.