We introduce a notion of strong proximity join-semilattice, a predicative notion of continuous lattice which arises as the Karoubi envelop of the category of algebraic lattices. Strong proximity join-semilattices can be characterised by the coalgebras of the lower powerlocale on the wider category of proximity posets (also known as abstract bases or R-structures). Moreover, locally compact locales can be characterised in terms of strong proximity join-semilattices by the coalgebras of the double powerlocale on the category of proximity posets. We also provide more logical characterisation of a strong proximity join-semilattice, called a strong continuous finitary cover, which uses an entailment relation to present the underlying join-semilattice. We show that this structure naturally corresponds to the notion of continuous lattice in the predicative point-free topology. Our result makes the predicative and finitary aspect of the notion of continuous lattice in point-free topology more explicit.

翻译：我们引入了强烈近距离联合空间概念,这是卡鲁比对升降层类别包罗的卡鲁比对连续岩层的预言性概念。强烈近距离联合岩层的特征可以是更广大的近距离岩层(也称为抽象基础或R结构)上的低功率地区对更广大的近距离岩层(也称为 " 抽象基础 " 或 " R-结构 " )的煤层对接。此外,地方紧凑地区对近距离联合岩层的描述可以是近距离联合岩层的强烈接近岩层。我们还提供了更符合逻辑的强烈近距离联合岩层的特征,称为强烈的连续岩层覆盖,它利用一种必然关系来展示潜在的联合岩层。我们表明,这一结构自然与预定点自由地表层中连续粘结的概念相对应。我们的结果使得近点表层持续粘结概念的先入为主和直线的方面更加明确。