形式化压缩数学的范畴基础

压缩数学由克劳森和施尔克泊过去几年发展而来，提出了一种对拓扑学的概括，其具有更好的范畴属性。它将拓扑空间的概念替换为压缩集的概念，后者可定义为针对某一类别中紧致华氏空间的共现拓扑的表层。就此而言，表层条件具有相当简单的明确描述，这源于研究共现、正规和广泛拓扑之间的关系。在本文中，我们在最低限度的假设下建立了该关系，超越紧致华氏空间的案例。顺便我们还提供了表层和覆盖筛的表征。本文中所有结果都在Lean证明助手中得到了完全形式化。