Skip to content

Commit dde8dbf

Browse files
chore: add references for order types (leanprover-community#34739)
1 parent e120823 commit dde8dbf

3 files changed

Lines changed: 25 additions & 6 deletions

File tree

Mathlib/Order/Types/Arithmetic.lean

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,10 @@ The following are notations in the `OrderType` namespace:
3030
## References
3131
3232
* <https://en.wikipedia.org/wiki/Order_type>
33-
* Dauben, J. W. Georg Cantor: His Mathematics and Philosophy of the Infinite. Princeton,
34-
NJ: Princeton University Press, 1990.
35-
* Enderton, Herbert B. Elements of Set Theory. United Kingdom: Academic Press, 1977.
33+
* [Dauben, J. W., Georg Cantor: His Mathematics and Philosophy of the Infinite. Princeton,
34+
NJ: Princeton University Press, 1990.][dauben_1990]
35+
* [Enderton, Herbert B., Elements of Set Theory. United Kingdom: Academic Press,
36+
1977.][enderton_1977]
3637
3738
## Tags
3839

Mathlib/Order/Types/Defs.lean

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,10 @@ The following are notations in the `OrderType` namespace:
3030
## References
3131
3232
* <https://en.wikipedia.org/wiki/Order_type>
33-
* Dauben, J. W. Georg Cantor: His Mathematics and Philosophy of the Infinite. Princeton,
34-
NJ: Princeton University Press, 1990.
35-
* Enderton, Herbert B. Elements of Set Theory. United Kingdom: Academic Press, 1977.
33+
* [Dauben, J. W., Georg Cantor: His Mathematics and Philosophy of the Infinite. Princeton,
34+
NJ: Princeton University Press, 1990.][dauben_1990]
35+
* [Enderton, Herbert B., Elements of Set Theory. United Kingdom: Academic Press,
36+
1977.][enderton_1977]
3637
3738
## Tags
3839

docs/references.bib

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1443,6 +1443,15 @@ @Article{ crans2017
14431443
url = {https://doi.org/10.1007/s40062-016-0164-9}
14441444
}
14451445

1446+
@Book{ dauben_1990,
1447+
place = {Princeton, NJ},
1448+
title = {Georg Cantor: His Mathematics and Philosophy of the
1449+
Infinite},
1450+
publisher = {Princeton University Press},
1451+
author = {Dauben, Joseph W.},
1452+
year = {1990}
1453+
}
1454+
14461455
@Book{ davey_priestley,
14471456
author = {Davey, B. A. and Priestley, H. A.},
14481457
title = {Introduction to lattices and order},
@@ -1746,6 +1755,14 @@ @Article{ elliott2006binomial
17461755
doi = {10.1016/j.jpaa.2005.09.003}
17471756
}
17481757

1758+
@Book{ enderton_1977,
1759+
place = {New York},
1760+
title = {Elements of set theory},
1761+
publisher = {Academic Press},
1762+
author = {Enderton, Herbert B.},
1763+
year = {1977}
1764+
}
1765+
17491766
@Book{ engel1997,
17501767
title = {Sperner theory},
17511768
author = {Engel, Konrad},

0 commit comments

Comments
 (0)