A General Constructive Proof Technique
Douglas Bridges, Luminiţa Vı̂ţă · Electronic Notes in Theoretical Computer Science · 2005
In the constructive theory of uniform spaces there occurs a technique of proof in which the application of a weak form of the law of excluded middle is circumvented by purely analytic means. The essence of this proof–technique is extracted and then applied to three important problems in the theory of apartness and uniformity.