[FOM] constructive Tychonov

Andrej Bauer Andrej.Bauer at fmf.uni-lj.si
Wed Nov 28 10:54:21 EST 2007

Robert Black wrote:
> Is there a constructively provable version of the Tychonov product 
> theorem? And if there is, exactly what does it say, and what 
> definition of 'compact' does it use?

Yes, see for example Steve Vicker's "Some constructive roads to
Tychonoff", published in "From Sets and Types to Topology and Analysis:
Towards Practicable Foundations for Constructive Mathematics", Edited by
Laura Crosilla and Peter Schuster, Oxford University Press, 2005,

The paper can be downloaded at

Best regards,


More information about the FOM mailing list