Homotopy Type Theory
Cauchy approximation > history (Rev #9, changes)
Showing changes from revision #8 to #9:
Added | Removed | Changed
Definition
Let A R A R be a dense integral subdomain of the dense rational numbers Archimedean ordered abelian group ℚ \mathbb{Q} with and a let point 1 R + : A 1:A R_{+} and be a the term positive terms of ζ R : 0 < 1 \zeta: R 0 \lt 1. Let A + ≔ ∑ a : A ( 0 < a ) A_{+} \coloneqq \sum_{a:A} (0 \lt a) be the positive cone? of A A
Let S S A R + A_{+} R_{+} premetric space . We define the predicate
isCauchyApproximation ( x ) ≔ ∏ δ : A R + ∏ η : A R + x δ ∼ δ + η x η isCauchyApproximation(x) \coloneqq \prod_{\delta:A_{+}} \prod_{\delta:R_{+}} \prod_{\eta:A_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\eta x x A R + A_{+} R_{+}
x : A R + → S ⊢ c ( x ) : isCauchyApproximation ( x ) x:A_{+} x:R_{+} \to S \vdash c(x): isCauchyApproximation(x)The type of A R + A_{+} R_{+} S S
C ( S , A R + ) ≔ ∑ x : A R + → S isCauchyApproximation ( x ) C(S, A_{+}) R_{+}) \coloneqq \sum_{x:A_{+} \sum_{x:R_{+} \to S} isCauchyApproximation(x) Properties
Every A R + A_{+} R_{+} Cauchy net indexed by A R + A_{+} R_{+} A R + A_{+} R_{+} N : A R + N:A_{+} N:R_{+} N ≔ δ ⊗ η N \coloneqq \delta \otimes \eta δ : A R + \delta:A_{+} \delta:R_{+} η : A R + \eta:A_{+} \eta:R_{+} ϵ : R + \epsilon:R_{+} ϵ + δ ⊕ η \epsilon + \delta \oplus \eta
Thus, there is a family of dependent terms
x : A R + → S ⊢ n ( x ) : isCauchyApproximation ( x ) → isCauchyNet ( x ) x:A_{+} x:R_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x) A An A R + A_{+} R_{+} x ∘ M x \circ M x x and a an A R + A_{+} R_{+} modulus of Cauchy convergence M M
See also
References
Revision on March 31, 2022 at 02:35:32 by
Anonymous? .
See the history of this page for a list of all contributions to it.