author | wenzelm |
Mon, 11 Sep 2023 19:30:48 +0200 | |
changeset 78659 | b5f3d1051b13 |
parent 74475 | 409ca22dee4c |
child 79957 | ef635b035561 |
permissions | -rw-r--r-- |
69519 | 1 |
@article{dugundji, |
2 |
author = {J. Dugundji}, |
|
3 |
title = {An extension of {Tietze's} theorem}, |
|
4 |
journal = {Pacific J. Math.}, |
|
5 |
pages = {353-367}, |
|
6 |
volume = 1, |
|
7 |
number = 3, |
|
8 |
year = 1951, |
|
9 |
url = {https://projecteuclid.org/euclid.pjm/1103052106}} |
|
10 |
||
70953 | 11 |
@article{DBLP:journals/jar/Maggesi18, |
12 |
author = {Marco Maggesi}, |
|
13 |
title = {A Formalization of Metric Spaces in {HOL} Light}, |
|
14 |
journal = {J. Autom. Reasoning}, |
|
15 |
volume = {60}, |
|
16 |
number = {2}, |
|
17 |
pages = {237--254}, |
|
18 |
year = {2018}, |
|
19 |
url = {https://doi.org/10.1007/s10817-017-9412-x}, |
|
20 |
doi = {10.1007/s10817-017-9412-x}, |
|
21 |
timestamp = {Thu, 25 Jan 2018 11:13:11 +0100}, |
|
22 |
biburl = {https://dblp.org/rec/bib/journals/jar/Maggesi18}, |
|
23 |
bibsource = {dblp computer science bibliography, https://dblp.org} |
|
24 |
} |
|
25 |
||
74475
409ca22dee4c
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents:
70953
diff
changeset
|
26 |
@book{conway2013course, |
409ca22dee4c
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents:
70953
diff
changeset
|
27 |
title={A course in functional analysis}, |
409ca22dee4c
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents:
70953
diff
changeset
|
28 |
author={Conway, John B}, |
409ca22dee4c
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents:
70953
diff
changeset
|
29 |
volume={96}, |
409ca22dee4c
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents:
70953
diff
changeset
|
30 |
year={2013}, |
409ca22dee4c
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents:
70953
diff
changeset
|
31 |
publisher={Springer Science \& Business Media} |
409ca22dee4c
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents:
70953
diff
changeset
|
32 |
} |
409ca22dee4c
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents:
70953
diff
changeset
|
33 |
|
69519 | 34 |
@misc{dummy} |