Abstract
We introduce the constructive notion of a uniformity (uniform structure) with the spirit of Sambin’s notion of a basic pair, and show some natural properties of a uniform space, a setoid with a uniform structure.
Then we construct a completion of a uniform space as a setoid of (regular) nets, define topological linear spaces and topological vector lattices as linear spaces and vector lattices equipped with uniform structures, and show that these algebraic and topological structures are preserved under the completion.
We introduce the notion of an abstract integration space consisting of a vector lattice and a positive linear functional.
By defining two uniform structures on an abstract integration space, we define corresponding topological vector lattices, and spaces of integration and measurable functions as the completion of these topological vector lattices.
Finally, we show some convergence theorems on these spaces such as Lebesgue’s monotone and dominated convergence theorems and Fatou’s lemma.
Talk Details
Speaker: Hajime Ishihara (Toho University, Japan)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Thursday 18 December 2025
Time: 10:20 (remote)
Key Topics
- Constructive mathematics
- Uniform structures
- Sambin’s basic pairs
- Topological vector lattices
- Integration theory
- Lebesgue convergence theorems
- Fatou’s lemma
- Abstract integration spaces
- Completion of uniform spaces
- Regular nets