Map · 06
order theory
MSC 06 · Order, lattices, ordered algebraic structures
32,568 declarations (27,277 theorems, 5,291 definitions) across 571 files. 6 of the 9 famous theorems listed for this area are in Mathlib (67%). 3 open conjectures here are stated in Lean.
Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.
Subareas6
- 06A Ordered sets 17,068
- 06F Ordered structures 8,146
- 06B Lattices 4,619
- 06E Boolean algebras (Boolean rings) 1,537
- 06D Distributive lattices 1,101
- 06C Modular lattices, complemented lattices 97
Famous theorems6 of 9
From the 1000+ theorems project, which classifies each theorem by MSC area.
Not yet in Mathlib · 3
In Mathlib · 6
- Birkhoff's representation theoremLatticeHom.birkhoffSet
- Bourbaki–Witt theoremChainCompletePartialOrder.nonempty_fixedPoints_of_inflationary
- Cantor's isomorphism theoremOrder.iso_of_countable_dense
- Hahn embedding theoremhahnEmbedding_isOrderedAddMonoid
- Kleene fixed-point theoremfixedPoints.lfp_eq_sSup_iterate
- Knaster–Tarski theoremfixedPoints.completeLattice
Open conjectures stated in Lean3
Statements without proofs, collected by the Formal Conjectures project.
- DedekindNumber.Dedekind_10Wikipedia
- DedekindNumber.M_eqWikipedia
Structures defined here24
Typeclasses defined in this area's files, most assumed first.
- Preorder 11,659
- LinearOrder 10,186
- PartialOrder 8,135
- IsStrictOrderedRing 2,839
- IsOrderedAddMonoid 1,934
- SetLike 1,706
- CompleteLattice 1,340
- Lattice 1,291
- OrderBot 1,254
- IsOrderedRing 929
- SemilatticeSup 926
- LocallyFiniteOrder 791
- SemilatticeInf 783
- Archimedean 683
- IsOrderedMonoid 675
- SuccOrder 675
- ConditionallyCompleteLinearOrder 626
- OrderTop 625
- DenselyOrdered 484
- BoundedOrder 481
- IsOrderedCancelAddMonoid 447
- FloorRing 430
- Nat.AtLeastTwo 421
- ConditionallyCompleteLattice 415
Files571
Largest first. The code after each file is its assigned subarea.
- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Ordered monoids
06F · 402
- Mathlib.Order.WithBot
`WithBot`, `WithTop`
06A · 369
- Mathlib.Data.Set.Lattice
The set lattice
06E · 347
- Mathlib.Order.CompleteLattice.Basic
Theory of complete lattices
06B · 327
- Mathlib.Algebra.Order.GroupWithZero.Basic
Lemmas on the monotone multiplication typeclasses
06F · 320
- Mathlib.Order.Hom.Basic
Order homomorphisms
06A · 317
- Mathlib.Data.Set.Image
Images and preimages of sets
06A · 313
- Mathlib.Data.Set.Function
Functions over sets
06A · 304
- Mathlib.Order.Heyting.Basic
Heyting algebras
06D · 300
- Mathlib.Order.Lattice
(Semi-)lattices
06B · 300
- Mathlib.Algebra.Order.Group.Synonym
Group structure on the order type synonyms
06F · 294
- Mathlib.Order.Basic
Basic definitions about `≤` and `<`
06A · 284