Homotopy Type Theory
Cauchy net > history (Rev #8, changes)
Showing changes from revision #7 to #8:
Added | Removed | Changed
Contents
Definition
In premetric spaces
Let T T be a directed type , and let S S be a T T -premetric space . Given a directed type I I , a net x : I → S x: I \to S is a Cauchy net if
x : I → S ⊢ c ( x ) : ∏ ϵ : T ‖ ∑ N : I ∏ i : I ∏ j : I ( i ≥ N ) × ( j ≥ N ) × ( x i ∼ ϵ x j ) ‖ x:I \to S \vdash c(x):\prod_{\epsilon:T} \Vert \sum_{N:I} \prod_{i:I} \prod_{j:I} (i \geq N) \times (j \geq N) \times (x_i \sim_{\epsilon} x_j) \Vert
Cauchy approximations
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) A net x : A + → S x: A_{+} \to S is a A + A_{+} -Cauchy approximation if
Let A + ≔ ∑ a : A ( 0 < a ) A_{+} \coloneqq \sum_{a:A} (0 \lt a) be the positive cone? of A A .
x : R + → S ⊢ c ( x ) : ∏ δ : R + ∏ η : R + x δ ∼ δ + η x η x:R_{+} \to S \vdash c(x):\prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\eta A Every netx : A + → S x: A_{+} \to S -Cauchy approximation is aA + A_{+} -Cauchy approximationCauchy net if 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 + \eta .
x : R + → S ⊢ c ( x ) : ∏ δ : R + ∏ η : R + x δ ∼ δ + η x η x:R_{+} \to S \vdash c(x):\prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\eta
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 .
In Cauchy spaces
…
Cauchy sequences
A Cauchy sequence is a Cauchy net whose index type is the natural numbers ℕ \mathbb{N} .
See also
Revision on March 12, 2022 at 22:10:31 by
Anonymous? .
See the history of this page for a list of all contributions to it.