chore(order/omega_complete_partial_order): clean up references (#7781)

fix the references rendering by adding them to the .bib

docs/references.bib

@@ -120,21 +120,20 @@ @InProceedings{   beylin1996
   isbn          = "978-3-540-70722-6"
 }
 
-@book {billingsley1999,
-    AUTHOR = {Billingsley, Patrick},
-     TITLE = {Convergence of probability measures},
-    SERIES = {Wiley Series in Probability and Statistics: Probability and
-              Statistics},
-   EDITION = {Second},
-      NOTE = {A Wiley-Interscience Publication},
- PUBLISHER = {John Wiley \& Sons, Inc., New York},
-      YEAR = {1999},
-     PAGES = {x+277},
-      ISBN = {0-471-19745-9},
-   MRCLASS = {60B10 (28A33 60F17)},
-  MRNUMBER = {1700749},
-       DOI = {10.1002/9780470316962},
-       URL = {https://doi.org/10.1002/9780470316962},
+@Book {           billingsley1999,
+  author        = {Billingsley, Patrick},
+  title         = {Convergence of probability measures},
+  series        = {Wiley Series in Probability and Statistics: Probability and Statistics},
+  edition       = {Second},
+  note          = {A Wiley-Interscience Publication},
+  publisher     = {John Wiley \& Sons, Inc., New York},
+  year          = {1999},
+  pages         = {x+277},
+  isbn          = {0-471-19745-9},
+  mrclass       = {60B10 (28A33 60F17)},
+  mrnumber      = {1700749},
+  doi           = {10.1002/9780470316962},
+  url           = {https://doi.org/10.1002/9780470316962},
 }
 
 @Book{            borceux-vol1,
@@ -196,6 +195,18 @@ @Book{            bourbaki1975b
   mrnumber      = {2109105}
 }
 
+@Article{         cadiou1972,
+  title         = {Recursive definitions of partial functions and their computations},
+  doi           = {10.1145/942580.807072},
+  number        = {14},
+  journal       = {ACM SIGACT News},
+  author        = {Cadiou, Jean Marie Cadiou and Manna, Zohar},
+  year          = {1972},
+  month         = {Jan},
+  pages         = {58–65}
+}
+
+
 @Book{            calugareanu,
   author        = {C\v{a}lug\v{a}reanu, Grigore},
   year          = {2000},
@@ -385,8 +396,7 @@ @InProceedings{   Gallier2011Notes
 
 @Article{         ghys87:groupes,
   author        = {Étienne Ghys},
-  title         = {Groupes d'homeomorphismes du cercle et cohomologie
-                  bornee},
+  title         = {Groupes d'homéomorphismes du cercle et cohomologie bornée},
   journal       = {Contemporary Mathematics},
   year          = 1987,
   volume        = 58,
@@ -423,6 +433,15 @@ @Book{            Gratzer2011
   mrnumber      = {2768581}
 }
 
+@Book{            gunter1992,
+  title         = {Semantics of Programming Languages: Structures and Techniques},
+  isbn          = {0262570955},
+  publisher     = {MIT Press},
+  author        = {Gunter, Carl A.},
+  year          = {1992}
+}
+
+
 @Article{         Gusakov2021,
   author        = {Alena Gusakov and Bhavik Mehta and Kyle A. Miller},
   title         = {Formalizing Hall's Marriage Theorem in Lean},
@@ -621,6 +640,19 @@ @Book{            marcus1977number
   publisher     = {Springer}
 }
 
+@article{         markowsky1976,
+  title         = {Chain-complete posets and directed sets with applications},
+  volume        = {6},
+  DOI           = {10.1007/bf02485815},
+  number        = {1},
+  journal       = {Algebra Universalis},
+  author        = {Markowsky, George},
+  year          = {1976},
+  month         = {Dec},
+  pages         = {53–68}
+}
+
+
 @InProceedings{   mcbride1996,
   title         = {Inverting inductively defined relations in {LEGO}},
   author        = {McBride, Conor},

src/order/omega_complete_partial_order.lean

@@ -46,9 +46,9 @@ supremum helps define the meaning of recursive procedures.
 
 ## References
 
- * [G. Markowsky, *Chain-complete posets and directed sets with applications*, https://doi.org/10.1007/BF02485815][markowsky]
- * [J. M. Cadiou and Zohar Manna, *Recursive definitions of partial functions and their computations.*, https://doi.org/10.1145/942580.807072][cadiou]
- * [Carl A. Gunter, *Semantics of Programming Languages: Structures and Techniques*, ISBN: 0262570955][gunter]
+ * [Chain-complete posets and directed sets with applications][markowsky1976]
+ * [Recursive definitions of partial functions and their computations][cadiou1972]
+ * [Semantics of Programming Languages: Structures and Techniques][gunter1992]
 -/
 
 universes u v
@@ -119,7 +119,7 @@ namespace omega_complete_partial_order
 
 /-- A chain is a monotonically increasing sequence.
 
-See the definition on page 114 of [gunter]. -/
+See the definition on page 114 of [gunter1992]. -/
 def chain (α : Type u) [preorder α] :=
 ℕ →ₘ α
 
@@ -188,7 +188,7 @@ operation on increasing sequences indexed by natural numbers (which we
 call `ωSup`). In this sense, it is strictly weaker than join complete
 semi-lattices as only ω-sized totally ordered sets have a supremum.
 
-See the definition on page 114 of [gunter]. -/
+See the definition on page 114 of [gunter1992]. -/
 class omega_complete_partial_order (α : Type*) extends partial_order α :=
 (ωSup     : chain α → α)
 (le_ωSup  : ∀(c:chain α), ∀ i, c i ≤ ωSup c)