Homotopy Type Theory
Cauchy net > history (Rev #7, changes)
Showing changes from revision #6 to #7:
Added | Removed | Changed
Contents
Definition
In premetric spaces
Let T T directed type , and let S S T T premetric space . Given a directed type I I x : I → S x: I \to S 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 T A T A directed abelian type group and with a point codirected type 1 : A 1:A , where a the directed type operation⊕ \oplus strict order is associative, and letS < S \lt , be a term T ζ : 0 < 1 T \zeta: 0 \lt 1 - and a family of dependent terms premetric space . A net x : T → S x: T \to S is a T T if
x a : R + A → , S b : A ⊢ c α ( x a , b ) : ∏ δ : R + ( ∏ η : R + 0 x δ < ∼ δ ⊕ η a x η ) × ( 0 < b ) → ( 0 < a + b ) x:R_{+} a:A, \to b:A S \vdash c(x):\prod_{\delta:R_{+}} \alpha(a, \prod_{\eta:R_{+}} b):(0 x_\delta \lt \sim_{\delta a) \oplus \times \eta} (0 x_\eta \lt b) \to (0 \lt a + b) Every Let T A + ≔ ∑ a : A ( 0 < a ) T A_{+} \coloneqq \sum_{a:A} (0 \lt a) -Cauchy approximation be is the aCauchy net positive cone? indexed of by T A T A . This is because T T is a codirected type, with N : T N:T defined as N ≔ δ ⊗ η N \coloneqq \delta \otimes \eta for δ : T \delta:T and η : T \eta:T . ϵ : R + \epsilon:R_{+} is defined as ϵ ≔ δ ⊕ η \epsilon \coloneqq \delta \oplus \eta
A net x : A + → S x: A_{+} \to S 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
Every A + A_{+} Cauchy net indexed by A + A_{+} A + A_{+} N : A + N:A_{+} N ≔ δ ⊗ η N \coloneqq \delta \otimes \eta δ : A + \delta:A_{+} η : A + \eta:A_{+} ϵ : R + \epsilon:R_{+} ϵ + δ ⊕ η \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 21:32:23 by
Anonymous? .
See the history of this page for a list of all contributions to it.