Homotopy Type Theory
Cauchy approximation > history (Rev #2)
Definition
Let R R be a Archimedean ordered integral domain with a dense strict order , and let R + R_{+} be the semiring? of positive terms in R R .
Suppose S S is a R + R_{+} -premetric space , and let x : R + → S x:R_{+} \to S be a net with index type R + R_{+} . We define the predicate
isCauchyApproximation ( x ) ≔ ‖ ∏ δ : R + ∏ η : R + x δ ∼ δ + η x ϵ ‖ isCauchyApproximation(x) \coloneqq \Vert \prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\epsilon \Vert
x x is a R + R_{+} -Cauchy approximation if
x : R + → S ⊢ c ( x ) : isCauchyApproximation ( x ) x:R_{+} \to S \vdash c(x): isCauchyApproximation(x)
The type of R + R_{+} -Cauchy approximations in S S is defined as
C ( S , R + ) ≔ ∑ x : R + → S isCauchyApproximation ( x ) C(S, R_{+}) \coloneqq \sum_{x:R_{+} \to S} isCauchyApproximation(x)
Properties
Every R + R_{+} -Cauchy approximation is a Cauchy net indexed by R + R_{+} . This is because R + R_{+} is a linear order , and thus a meet-pseudosemilattice, with N : R + N:R_{+} defined as N ≔ min ( δ , η ) N \coloneqq \min(\delta, \eta) for δ : R + \delta:R_{+} , η : R + \eta:R_{+} , and meet operation min : R + × R + → R + \min:R_{+} \times R_{+} \to R_{+} . ϵ : R + \epsilon:R_{+} is defined as ϵ ≔ δ + η \epsilon \coloneqq \delta + \eta .
Thus, there is a family of dependent terms
x : R + → S ⊢ n ( x ) : isCauchyApproximation ( x ) → isCauchyNet ( x ) x:R_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)
See also
References
Revision on March 11, 2022 at 20:59:18 by
Anonymous? .
See the history of this page for a list of all contributions to it.