Homotopy Type Theory
Cauchy approximation > history (Rev #8, changes)
Showing changes from revision #7 to #8:
Added | Removed | Changed
Definition
Let A A be a abelian dense group with a point1 : A 1:A Archimedean ordered abelian group , with a point strict order 1 : A 1:A and a term ζ : 0 < 1 \zeta: 0 \lt 1 , . a Let termζ A + : ≔ ∑ a : A ( 0 < 1 a ) \zeta: A_{+} 0 \coloneqq \sum_{a:A} (0 \lt 1 a) and be a the family of dependent terms positive cone? of A A .
a : A , b : A ⊢ α ( a , b ) : ( 0 < a ) × ( 0 < b ) → ( 0 < a + b ) a:A, b:A \vdash \alpha(a, b):(0 \lt a) \times (0 \lt b) \to (0 \lt a + b) Let S S be a A + A_{+} -premetric space . We define the predicate
Let A + ≔ ∑ a : A ( 0 < a ) A_{+} \coloneqq \sum_{a:A} (0 \lt a) be the positive cone? of A A .
isCauchyApproximation ( x ) ≔ ∏ δ : A + ∏ η : A + x δ ∼ δ + η x η isCauchyApproximation(x) \coloneqq \prod_{\delta:A_{+}} \prod_{\eta:A_{+}} x_\delta \sim_{\delta + \eta} x_\eta Let x x S S is a be a A + A_{+} -Cauchy approximationA + A_{+} if -premetric space . We define the predicate
x : A + → S ⊢ c ( x ) : isCauchyApproximation ( x ) ≔ ∏ δ : A + ∏ η : A + x δ ∼ δ ⊕ η x η x:A_{+} \to S \vdash c(x): isCauchyApproximation(x) \coloneqq \prod_{\delta:A_{+}} \prod_{\eta:A_{+}} x_\delta \sim_{\delta \oplus \eta} x_\eta
x x The type of is a A + A_{+} A + A_{+} -Cauchy approximation-Cauchy approximations in ifS S is defined as
x C : A + → S ⊢ c ( x S , A + ) : ≔ ∑ x : A + → S isCauchyApproximation ( x ) x:A_{+} C(S, A_{+}) \coloneqq \sum_{x:A_{+} \to S S} \vdash c(x): isCauchyApproximation(x)
The type of A + A_{+} -Cauchy approximations in S S is defined as
C ( S , A + ) ≔ ∑ x : A + → S isCauchyApproximation ( x ) C(S, A_{+}) \coloneqq \sum_{x:A_{+} \to S} isCauchyApproximation(x)
Properties
Every A + A_{+} -Cauchy approximation is a Cauchy net indexed by A + A_{+} . This is because A + A_{+} is a strictly ordered type, and thus a directed type and a strictly codirected type, with N : A + N:A_{+} defined as N ≔ δ ⊗ η N \coloneqq \delta \otimes \eta for δ : A + \delta:A_{+} and η : A + \eta:A_{+} . ϵ : R + \epsilon:R_{+} is defined as ϵ + δ ⊕ η \epsilon + \delta \oplus \eta .
Thus, there is a family of dependent terms
x : A + → S ⊢ n ( x ) : isCauchyApproximation ( x ) → isCauchyNet ( x ) x:A_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)
A A + A_{+} -Cauchy approximation is the composition x ∘ M x \circ M of a net x x and a A + A_{+} -modulus of Cauchy convergence M M .
See also
References
Revision on March 12, 2022 at 22:12:09 by
Anonymous? .
See the history of this page for a list of all contributions to it.