#scholze
A mathematical formalisation challenge by Peter Scholze(xenaproject.wordpress.com)
2020-12-6 21:16
这是Peter Scholze撰写的客座帖子，解释了液体实向量空间数学形式化挑战。有关挑战的pdf版本，请参见此处。有关形式化的注释，请参见第6节。现在转到Peter。
定理1.1（Clausen-S。）让我们成为实数，让它成为一个有限集，并让它成为-Banach空间。设为的度量空间。然后
（这是在www......