18. Теорема Гейне-Бореля о покрытиях

Замкнутое множество на вещественной прямой ограничено, если мы можем найти натуральное

число такое, что содержится в замкнутом интервале от до Определение для евклидова пространства аналогично. Ограниченное замкнутое множество в евклидовом пространстве, а также любое замкнутое множество в канторовском пространстве называются компактными.

Пусть компактное множество, и допустим, что

где последовательность открытых множеств. Тогда можно найти натуральное такое, что

Доказательство для канторового пространства. По предположению, где открыто и

Система Поста, определяющая левый член, состоит из отмеченных схем для схем для последовательности отмеченных, например, символом и новых схем

Любая окрестность, в частности , порождается этой системой Поста. Пусть максимум натуральных чисел, подставленных вместо в тех применениях последней схемы, которые входят в доказательство . Тогда, очевидно,

так что

что и требовалось доказать.

Конструктивная форма теоремы Гейне — Бореля была найдена Брауэром в [9]. Он доказал ее как следствие теоремы о веерах для так называемых локализованных компактных видов (Katalogisiertkompakte Species). Предположение локализованности (понятие локализованности будет введено в следующем разделе) излишне, по крайней мере в случае, если принята наша интерпретация интуиционистских понятий.