Homotopy Type Theory
sequentially Hausdorff space > history (Rev #1)
Contents
Definition
In Archimedean ordered fields
Let F F be an Archimedean ordered field . Then F F is a sequentially Hausdorff space if for all sequence s x : ℕ → F x:\mathbb{N} \to F , the type of all limits of x x is a proposition
isSequentiallyHausdorff ( F ) ≔ ∏ x : ℕ → F isProp ( lim n → ∞ x ( n ) ) isSequentiallyHausdorff(F) \coloneqq \prod_{x:\mathbb{N} \to F} isProp(\lim_{n \to \infty} x(n))
All Archimedean ordered fields are sequentially Hausdorff spaces.
Most general definition
Let S S be a type with a predicate → \to between the type of sequences in S S , ℕ → S \mathbb{N} \to S , and S S itself. Then S S is a sequentially Hausdorff space if for all sequence s x : ℕ → S x:\mathbb{N} \to S , the type of all limits of x x is a proposition
isSequentiallyHausdorff ( S ) ≔ ∏ x : ℕ → S isProp ( ∑ l : S x → l ) isSequentiallyHausdorff(S) \coloneqq \prod_{x:\mathbb{N} \to S} isProp\left(\sum_{l:S} x \to l\right)
One could directly define the limit lim n → ∞ ( − ) ( n ) \lim_{n \to \infty} (-)(n) as a partial function
lim n → ∞ ( − ) ( n ) : ( ℕ → S ) → 𝒰 S \lim_{n \to \infty} (-)(n): (\mathbb{N} \to S) \to_{\mathcal{U}} S
See also
Revision on March 31, 2022 at 17:32:34 by
Anonymous? .
See the history of this page for a list of all contributions to it.