Originally published at 狗和留美者不得入内. You can comment here or there.

**Definition 1** Take an interval . A *partition* of it is a finite sequence of real numbers .

**Definition 2** A partition is a *refinement of a partition* if it contains all the points of . Given any two partitions , one can always find their *common refinement*, which consists of all their points in increasing order.

**Definition 3** The *norm* or *mesh* of the partition is equal to

**Proposition 1** The collection of partitions of any closed interval is a directed set.

*Proof*: Under set inclusion, it is a preorder since reflexivity and transitivity are satisfied. The common refinement of any finite collection of partitions is always an upper bound of it.

**Definition 4** A *tagged partition* of , consists of , and for . A refinement of it is the same as the refinment of a partition with the additional requirement that the set of points inside the intervals of the refinement contains the .

**Proposition 2** The collection of tagged partitions of any closed interval is a directed set.

*Proof*: Similar as that of Proposition 1.

**Definition 5** The *Riemann sum* of a function corresponding to a tagged partition of , , , is given by

**Proposition 3** The collection of Riemann sums of a function is a net.

*Proof*: Proposition 2 tells us that the collection of tagged partitions of is a directed set, and the Riemann sum of is a function from this directed set to the reals.

**Definition 6** We say that a function is Riemann integrable if the net of Riemann sums associated with it converges to some real value . Equivalently, for all , there exists a tagged partition such that for any refinement of it, the distance between the Riemann sum and is less than .