CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> Editing sequence in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="noindex,nofollow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> Editing sequence </h1> <div id="MarkupHelp"> <h3 style="font-size: 1.1em; font-style: normal; text-align: center">Syntax tips</h3> <ol style="margin-left: 0em; padding-left: 0em"> <li style="font-size: 0.8em">The basic syntax is <a href="https://www.markdownguide.org/cheat-sheet/">extended Markdown</a>. </li> <li style="font-size: 0.8em">Links to other nLab pages should be made by surrounding the name of the page in double square brackets: [[ name of page ]]. To link to an nLab page but show a different link text, do the following: [[ name of page | link text to show ]].</li> <li style="font-size: 0.8em">LaTeX can be used inside single dollar signs (inline) or double dollar signs or \[ and \], as usual. </li> <li style="font-size: 0.8em">To create a table of contents, add \tableofcontents on its own line.</li> <li style="font-size: 0.8em">For a theorem or proof, use \begin{theorem} \end{theorem} as you would in LaTeX. Labelling and referencing is exactly as in LaTeX, with use of \label and \ref. The full list of supported environments can be found in the <a href="/nlab/show/HowTo#DefinitionTheoremProofEnvironments">HowTo</a>. </li> <li style="font-size: 0.8em">Tikz can be used for figures almost exactly as in LaTeX. Similarly, tikz-cd and xymatrix can be used for commutative diagrams. See the <a href="/nlab/show/HowTo#diagrams">HowTo</a>.</li> <li style="font-size: 0.8em">As an alternative to the Markdown syntax for sections (headings), one can use the usual LaTeX syntax \section, \subsection, etc.</li> <li style="font-size: 0.8em">For further help, see the <a href="/nlab/show/HowTo">HowTo</a>, or you are very welcome to ask at the <a href="https://nforum.ncatlab.org/">nForum</a>.</li> </ol> </div> <form accept-charset="utf-8" action="/nlab/save/sequence" id="editForm" method="post"> <div style="display: none;"> <input name="see_if_human" id="see_if_human" style="tabindex: -1; autocomplete: off"/> </div> <div> <textarea name="content" id="content" style="height: 45em; width: 70%;"> # Sequences * table of contents {: toc} ## Definitions A __sequence__ is a [[function]] whose [[source|domain]] is a [[subset]] of the set $\mathbb{N}$ of [[natural numbers]] (or more generally a subset of the set $\mathbb{Z}$ of [[integers]]; cf. *[[bi-infinite sequence]]* and the further generalizations [below](#Generalizations)). Often one means an __infinite sequence__, which is a sequence whose domain is infinite. Sequences (especially finite ones) are often called __[[lists]]__ in computer science. (In [[constructive mathematics]], the domain of a sequence must be a [[decidable subset]] of $\mathbb{Z}$.) Sequences may also be indicated by functions $\omega \to X$ where $\omega$ is the first countably infinite [[ordinal]]: the key piece of structure on $\mathbb{N}$ relevant for the study of sequences, particularly in analysis, is the order structure. Up to [[bijection]], the only possible [[domains]] are those of the form $$ \{i\colon \mathbb{Z} \;|\; 0 \leq i \lt n\} $$ for $n = 0, 1, 2, \ldots, \infty$; other domains are used for notational convenience. An alternative generalisation takes the domain to be a set of [[ordinal numbers]], without loss of generality the set $$ \{i\colon \Ord \;|\; i \lt \alpha\} $$ for $\alpha$ some specific ordinal number (or the [[proper class]] $\Ord$ of all ordinal numbers, if one wishes to allow for a proper class). A _subsequence_ of a sequence $a = a_n: \mathbb{N} \to X$ is a composition $$\mathbb{N} \stackrel{i}{\to} \mathbb{N} \stackrel{a}{\to} X$$ where $i$ is an order-preserving monomorphism. The salient point is that $i$ be [[cofinal diagram|cofinal]] as an embedding. ## Notation One normally writes the value of the sequence $a$ at the argument $i$ as $a_i$ rather than $a(i)$. Similarly, given a term $a[i]$ with the free variable $i$, one often defines a sequence whose values equal those terms as $(a[i])_{i \lt n}$, $\{a[i]\}_i$, or the like. In fact, one even often says literally 'Let $(a_i)$ be a sequence.' even though 'Let $a$ be a sequence.' would be less of an abuse of notation. This is all because notation for sequences arose before [[functions]] were considered in their full generality, and one distinguished a 'sequence' (whose domain was a set of integers) from a 'function' (whose domain was an interval in the real line or a region in the complex plane). Early mathematicians also often conflated the sequence (the function itself) with its range (a subset of the function\'s [[target]]); hence the use of curly braces. All of this applies in greater generality to [[families]] with index sets other than $\mathbb{N}$. ## Generalisations {#Generalization} ### Nets Infinite sequences are often used in [[topology]], but for topology in general, one needs to generalise to [[nets]], also called _Moore--Smith sequences_. Here one replaces the domain $\mathbb{N}$ by any arbitrary [[direction|directed set]]. ### Sequential nets Recall that [[weak countable choice]] is a rather weak version of the [[axiom of choice]] that is accepted even in most schools of [[constructive mathematics]]; it follows separately from both [[excluded middle]] and [[countable choice]]. However, when it fails (as it does in the [[internal language]] of some widely studied [[toposes]], such as the [[topos of sheaves]] over the [[real line]]), then some important results about sequences fail, including many standard results in [[topology]]. In this case, we may want a slight generalisation that we call _sequential nets_. A __[[sequential net]]__ is a [[multi-valued function]] from $\mathbb{N}$ (or a [[decidable subset|decidable]] [[subset]] thereof) to $X$, that is a [[span]] $\mathbb{N} \leftarrow A \rightarrow X$ where the map $A \to \mathbb{N}$ is a [[surjection]] (or has a decidable range). Note that $A$ inherits the structure of a directed set via $A \to \mathbb{N}$, so that $A \to X$ is a net. As a net, every sequential net is equivalent (in the sense of corresponding to the same [[filter]]) to some sequence, if you assume WCC. Without WCC, however, this equivalence fails. (Using a multi-valued function here is a special case of an alternative definition of [[net]] that uses only [[partially ordered]] directed sets; see [[net]]. In some [[foundations of mathematics]], we can get the same result by defining a sequential net to be a __presequence__: a [[prefunction]], which is like a function but need not preserve [[equality]], from $\mathbb{N}$ or a decidable subset thereof.) Without WCC, many of the usual properties of [[metric spaces]] and other [[sequential spaces]] fail, but they continue to hold using sequential nets in the place of sequences. For example, every (located Dedekind) [[real number]] may be represented as a sequential Cauchy net, even when they might not all be represented as Cauchy sequences; see [[Cauchy real number]]. ## Sequence types In [[dependent type theory]], a sequence type is simply the [[function type]] $\mathbb{N} \to A$, and thus comes with the following rules: Formation rules for sequence types: $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathbb{N} \to A \; \mathrm{type}}$$ Introduction rules for sequence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, n:\mathbb{N} \vdash a(n):A}{\Gamma \vdash \lambda(n:\mathbb{N}).a(n):\mathbb{N} \to A}$$ Elimination rules for sequence types: $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:\mathbb{N} \to A, n:\mathbb{N} \vdash \mathrm{ev}(a, n):A}$$ Computation rules for sequence types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, n:\mathbb{N} \vdash a(n):A}{\Gamma, m:\mathbb{N} \vdash \beta_\Pi(m):\mathrm{ev}(\lambda(n:\mathbb{N}).a(n), m) =_{A} a(m)}$$ Uniqueness rules for sequence types: $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:\mathbb{N} \to A \vdash \eta_\Pi(a):a =_{\mathbb{N} \to A} \lambda(n:\mathbb{N}).a(n)}$$ Sequence types also have their own extensionality principle, called [[sequence extensionality]]. This states that given two sequences $a:\mathbb{N} \to A$ and $b:\mathbb{N} \to A$ there is an [[equivalence of types]] between the [[identity type]] $a =_{\mathbb{N} \to A} b$ and the [[dependent sequence type]] $(n:\mathbb{N}) \to (a(n) =_{A} b(n))$: $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:\mathbb{N} \to A, b:\mathbb{N} \to A \vdash \mathrm{seqext}(a, b):(a =_{\mathbb{N} \to A} b) \simeq (n:\mathbb{N}) \to (a(n) =_{A} b(n))}$$ Sequence types are used in [[strongly predicative mathematics]], where one does not have [[function types]], to construct the [[real numbers]]. ## Sequence spaces In [[functional analysis]], one considers [[topological vector spaces]] of infinite sequences; these are the [[sequence spaces]]. (Actually, these generalise quite nicely to [[net]] spaces.) ## Related concepts * [[limit of a sequence]] * [[sequentially compact space]] * [[sequence algebra]] * [[sequential net]] * [[tuple]], **sequence**, [[function]] * [[dependent tuple]], [[dependent sequence]], [[dependent function]] Not all that related, but similar sounding: * [[sequential limit]] [[!redirects sequence]] [[!redirects sequences]] [[!redirects infinite sequence]] [[!redirects infinite sequences]] [[!redirects sequence type]] [[!redirects sequence types]] [[!redirects presequence]] [[!redirects presequences]] [[!redirects pre-sequence]] [[!redirects pre-sequences]] [[!redirects subsequence]] [[!redirects subsequences]] [[!redirects sub-sequence]] [[!redirects sub-sequences]] </textarea> <p> <input id="alter_title" name="alter_title" onchange="toggleVisibility();" type="checkbox" value="1" /> <label for="alter_title">Change page name.</label><br/> <span id="title_change" style="display:none"><label for="new_name">New name:</label> <input id="new_name" name="new_name" onblur="addRedirect();" type="text" value="sequence" /></span> </p> <div> <p style="font-size: 0.8em; width: 70%;"> For non-trivial edits, please briefly describe your changes below. A discussion thread for this page does not yet exist at the <a href="https://nforum.ncatlab.org/discussions/?CategoryID=0">nForum</a>, but will be created upon submission of your changes, and your comments will be added to it. This discussion thread can also be used for further discussion related to this page. For trivial edits, such as correcting typos, please leave the box below empty; feel free to ask for advice at the nForum if you are unsure. </p> </div> <div> <textarea name="announcement" id="announcement" style="height: 10em; width: 70%"></textarea> </div> <div id="editFormButtons"> <input type="submit" value="Submit" accesskey="s"/> as <input id="author" name="author" onblur="this.value == '' ? this.value = 'Anonymous' : true" onfocus="this.value == 'Anonymous' ? this.value = '' : true;" type="text" value="Anonymous" /> | <span> <a href="/nlab/cancel_edit/sequence" accesskey="c">Cancel</a> <span class="unlock">(unlocks page)</span> </span> </div> </div> </form> <script type="text/javascript"> <![CDATA[//><!]]> </script> </div>  </div>  </body> </html>