A Constructive View of Complete Regularity
Bernhara Banaschewski, Aleš Pultr · 2003
This note introduces the largest interpolative relation contained in the rather below (= well inside) relation in a frame as a constructive version of the familiar completely below (= really inside) relation. It establishes several constructively valid results for this whose analogues for the latter are only proved by means of the Axiom of Countable Dependent Choice.