diff --git a/Mathlib/Algebra/Order/Quantale.lean b/Mathlib/Algebra/Order/Quantale.lean index cc2e37662851c..449dd9074001d 100644 --- a/Mathlib/Algebra/Order/Quantale.lean +++ b/Mathlib/Algebra/Order/Quantale.lean @@ -11,7 +11,7 @@ import Mathlib.Order.CompleteLattice Quantales are the non-commutative generalization of locales/frames and as such are linked to point-free topology and order theory. Applications are found throughout logic, -quantum mechanics, and computer science. +quantum mechanics, and computer science (see e.g. [Vickers1989] and [Mulvey1986]). The most general definition of quantale occurring in literature, is that a quantale is a semigroup distributing over a complete sup-semilattice. In our definition below, we use the fact that diff --git a/docs/references.bib b/docs/references.bib index 9aced0385241a..5ff2fe08d22a1 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -2701,6 +2701,21 @@ @Article{ MR577178 url = {https://doi.org/10.1007/BF00417500} } +@Article{ Mulvey1986, + Author = {Mulvey, Christopher J.}, + Title = {\&}, + FJournal = {Supplemento ai Rendiconti del Circolo Matem{\`a}tico di Palermo. Serie II}, + Journal = {Suppl. Rend. Circ. Mat. Palermo (2)}, + ISSN = {1592-9531}, + Volume = {12}, + Pages = {99--104}, + Year = {1986}, + Language = {English}, + Keywords = {46L60,46L05,81Q10}, + zbMATH = {4030272}, + Zbl = {0633.46065} +} + @Unpublished{ Naor-2015, author = {Assaf Naor}, title = {Metric Embeddings and Lipschitz Extensions}, @@ -3301,6 +3316,15 @@ @Book{ verdier1996 mrnumber = {1453167} } +@Book{ Vickers1989, + author = {Vickers, Steven}, + title = {Topology via Logic}, + isbn = {0-521-57651-2}, + year = {1989}, + publisher = {University of Cambridge}, + language = {English} +} + @Misc{ vistoli2004, author = {Vistoli, Angelo}, title = {Notes on {Grothendieck} topologies, fibered categories and @@ -3311,15 +3335,6 @@ @Misc{ vistoli2004 arxiv = {arXiv:math/0412512} } -@Book{ vickers1989, - author = {Vickers, Steven}, - title = {Topology via Logic}, - isbn = {0-521-57651-2}, - year = {1989}, - publisher = {University of Cambridge}, - language = {English} -} - @Book{ wall2018analytic, title = {Analytic Theory of Continued Fractions}, author = {Wall, H.S.},