nLab Richman premetric space

Contents

This entry is about 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. For the family of binary relations indexed by the positive rational numbers defined by Auke Booij in Analysis in univalent type theory.


Contents

Idea

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

Definition

A Richman premetric space is a set SS with a ternary relation () ()():S× 0×SΩ(-)\sim_{(-)}(-)\colon S \times \mathbb{Q}_{\geq 0} \times S \to \Omega, where 0\mathbb{Q}_{\geq 0} represent the non-negative rational numbers in \mathbb{Q} and Ω\Omega is the set of truth values, such that

  • for all xSx \in S and ySy \in S, (x=y)(x 0y)(x = y) \iff (x \sim_0 y)

  • for all xSx \in S and ySy \in S, there exists q 0q \in \mathbb{Q}_{\geq 0} such that x qyx \sim_q y

  • for all xSx \in S, ySy \in S, q 0q \in \mathbb{Q}_{\geq 0}, and r(q,)r \in (q, \infty), where (q,)(q, \infty) is the set of all non-negative rational numbers strictly greater than qq, then (x ry)(x qy)(x \sim_r y) \iff (x \sim_q y)

  • for all xSx \in S, ySy \in S, zSz \in S, q 0q \in \mathbb{Q}_{\geq 0}, and r 0r \in \mathbb{Q}_{\geq 0}, if x qyx \sim_q y and y rzy \sim_r z, then x q+rzx \sim_{q + r} z.

Properties

Assuming excluded middle, every Richman premetric space is a metric space. Without excluded middle, however, every Richman premetric space is a “metric space” which is valued in the lower Dedekind real numbers, rather than the two-sided Dedekind real numbers.

See also

References

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