This entry is about the family of binary relations indexed by the positive rational numbers defined by Auke Booij in Analysis in univalent type theory. For the family of binary relations indexed by the non-negative rational numbers defined by Fred Richman in Real numbers and other completions, see Richman premetric space.

**analysis** (differential/integral calculus, functional analysis, topology)

metric space, normed vector space

open ball, open subset, neighbourhood

convergence, limit of a sequence

compactness, sequential compactness

continuous metric space valued function on compact metric space is uniformly continuous

…

…

A more general concept of metric space by Auke Booij. While Auke Booij simply called these structures “premetric spaces”, there are multiple notions of premetric spaces in the mathematical literature, so we shall refer to these as Booij premetric spaces.

A **Booij premetric space** is a set $S$ with a ternary relation $(-)\sim_{(-)}(-)\colon S \times \mathbb{Q}_+ \times S \to \Omega$, where $\mathbb{Q}_+$ represent the positive rational numbers in $\mathbb{Q}$ and $\Omega$ is the set of truth values.

Booij premetric spaces are used as in the construction of the Cauchy real numbers and the HoTT book real numbers.

- Auke B. Booij, Analysis in univalent type theory (pdf)

Last revised on May 31, 2022 at 13:50:27. See the history of this page for a list of all contributions to it.