Showing changes from revision #7 to #8: Added | Removed | Changed

Contents

Definition

A sequence net is a net function whose index type is thenatural numbers$a \in A^I$ from a directed set$\mathrm{<span><del\; class="diffmod">\; \mathbb{N}</del><ins\; class="diffmod">\; I</ins></span>}$ \mathbb{N} I to a set $A$. $I$ is called the index set, the terms of $I$ are called indices (singular index), and $A$ is called the indexed set.

Examples

• The Cauchy approximations used to define the HoTT book real numbers are nets indexed by a dense subsemiring $R_{+}$ of the positive rational numbers $\mathbb{Q}_+$.

See also

• directed type

• Cauchy structure

• Cauchy net

• limit of a net