**
**

**Petrakis, Iosif (2016): The Urysohn Extension Theorem for Bishop Spaces. In: Logical Foundations of Computer Science: International Symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4-7, 2016. Proceedings.**

*Lecture Notes in Computer Science*, Vol. 9537. Cham: Springer. pp. 299-316**Full text not available from 'Open Access LMU'.**

## Abstract

Bishop's notion of function space, here called Bishop space, is a function-theoretic analogue to the classical set-theoretic notion of topological space. Bishop introduced this concept in 1967, without exploring it, and Bridges revived the subject in 2012. The theory of Bishop spaces can be seen as a constructive version of the theory of the ring of continuous functions. In this paper we define various notions of embeddings of one Bishop space to another and develop their basic theory in parallel to the classical theory of embeddings of rings of continuous functions. Our main result is the translation within the theory of Bishop spaces of the Urysohn extension theorem, which we show that it is constructively provable. We work within Bishop's informal system of constructive mathematics BISH, inductive definitions with countably many premises included.

Item Type: | Book Section |
---|---|

Faculties: | Mathematics, Computer Science and Statistics > Mathematics |

Subjects: | 500 Science > 510 Mathematics |

ISBN: | 978-3-319-27682-3 |

Place of Publication: | Cham |

Language: | English |

Item ID: | 47279 |

Date Deposited: | 27. Apr 2018, 08:12 |

Last Modified: | 04. Nov 2020, 13:24 |