Let RR be a Archimedean ordered integral domain with a dense linear order?, and let R +R_{+} be the semiring? of positive terms in RR. A R +R_{+}-premetric space is a type SS with a family of types
called the R +R_{+}-premetric, and a family of dependent terms
representing that the R +R_{+}-premetric is a predicate.
Cauchy structure
Cauchy net
Revision on March 11, 2022 at 18:52:44 by Anonymous?. See the history of this page for a list of all contributions to it.