In real analysis, a branch of mathematics, Cousin's theorem states that: This result was originally proved by Pierre Cousin, a student of Henri Poincaré, in 1895, and it extends the original Heine–Borel theorem on compactness for arbitrary covers of compact subsets of. However, Pierre Cousin did not receive any credit. Cousin's theorem was generally attributed to Henri Lebesgue as the Borel–Lebesgue theorem. Lebesgue was aware of this result in 1898, and proved it in his 1903 dissertation. In modern terms, it is stated as: Cousin's lemma is studied in reverse mathematics where it is one of the first third-order theorems that is hard to prove in terms of the comprehension axioms needed.

In Henstock–Kurzweil integration

Cousin's theorem is instrumental in the study of Henstock–Kurzweil integration, and in this context, it is known as Cousin's lemma or the fineness theorem. A gauge on [a,b] is a strictly positive real-valued function, while a tagged partition of [a,b] is a finite sequence Given a gauge and a tagged partition P of [a,b], we say P is \delta-fine if for all, we have , where B(x, r) denotes the open ball of radius r centred at x. Cousin's lemma is now stated as:

Proof of the theorem

Cousin's theorem has an intuitionistic proof using the open induction principle, which reads as follows: An open subset S of a closed real interval [a,b] is said to be inductive if it satisfies that implies. The open induction principle states that any inductive subset S of [a,b] must be the entire set.

Proof using open induction

Let S be the set of points r such that there exists a \delta-fine tagged partition on [a,s] for some s \geq r. The set S is open, since it is downwards closed and any point in it is included in the open ray for any associated partition. Furthermore, it is inductive. For any r, suppose. By that assumption (and using that either r > a or to handle the base case) we have a partition of length n with. Then either or x_n < b. In the first case, so we can just replace x_n with b and get a partition of [a,b] that includes r. If x_n < b, we may form a partition of length n+1 that includes r. To show this, we split into the cases r > x_n or. In the first case, we set t_{n+1} = r, in the second we set. In both cases, we can set and obtain a valid partition. So in all cases, and S is inductive. By open induction, S = [a,b].