Homotopy Type Theory
limit of a net > history (Rev #9, changes)
Showing changes from revision #8 to #9:
Added | Removed | Changed
Contents
Definition
In premetric spaces
Let T R T R be a dense integral subdomain of the directed rational type numbers , and let S ℚ S \mathbb{Q} be and a let T R + T R_{+} - be the positive terms of R R . Let S S be a R + R_{+} - premetric space . Given a directed type I I l : S l:S limit of a net x : I → S x: I \to S x x converges to l l l l
λ : ∏ ϵ : T R + ‖ ∑ N : I ∏ i : I ( i ≥ N ) → ( x i ∼ ϵ l ) ‖ \lambda: \prod_{\epsilon:T} \prod_{\epsilon:R_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_{\epsilon} l) \Vert A limit of a sequence a : ℕ → S a:\mathbb{N} \to S
lim x → ∞ a ( x ) \lim_{x \to \infty} a(x) Cauchy approximations
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
A limit of a A R + A_{+} R_{+} Cauchy approximation x : A R + → S x: A_{+} R_{+} \to S l : S l:S
x : A R + → S ⊢ c ( x ) : ∏ δ : A R + ∏ η : A R + x δ ∼ δ ⊕ η l x:A_{+} x:R_{+} \to S \vdash c(x):\prod_{\delta:A_{+}} c(x):\prod_{\delta:R_{+}} \prod_{\eta:A_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta \oplus \eta} lIn convergence spaces
…
See also
Revision on March 31, 2022 at 03:02:22 by
Anonymous? .
See the history of this page for a list of all contributions to it.