Глава 2. Топология и компактность

От метрики к топологии

Что построила предыдущая глава

Глава 5.1 дала Части V первое аналитическое понятие — расстояние. Появились метрика на рациональных числах, абстрактное метрическое пространство, расстояние как процесс и — в самом конце — первое обещание: открытые шары $B (P, ε)$ и понятие <<близких процессов>>. На этом обещании и начинается настоящая глава.

Имея расстояние, можно строить топологию — науку о близости, окрестности, форме. Топология отвечает на вопросы, которые метрика только готовит. Что значит, что множество <<открыто>> — что у каждой его точки есть запас свободного пространства вокруг? Что значит, что две точки можно отделить? Что значит, что множество <<связно>> — что из любой его точки можно пройти к любой другой, не покидая множества? И — центральное понятие главы — что значит, что множество компактно?

Два слоя главы: топология и компактность

Глава распадается на два слоя, и о различии между ними честнее сказать сразу, с самого начала.

Первый слой — собственно топология: открытые и замкнутые множества, отделимость, связность. Этот слой над $Q$ строится полностью и конструктивно. Опорные файлы топологического слоя — Topology.v, ProcessTopOpen.v, ProcessTop\- Connected.v — не используют ни одной аксиомы. Здесь ToS получает топологию <<даром>>: из одного только рационального расстояния, без всяких дополнительных допущений.

Второй слой — компактность: теоремы Гейне–Бореля и Больцано–Вейерштрасса. И вот здесь картина меняется. Компактность — то место, где рациональные числа обнаруживают свою неполноту. Классический Гейне–Борель над $Q$ попросту неверен (об этом — § 2.5), и теоремы компактности приходится либо ремонтировать, либо доказывать с привлечением законов логики ToS. Файлы компактностного слоя — HeineBorel_ERR.v, BolzanoWeierstrass.v — опираются на $L 3$ и локально на $L 4$ .

Глава честно держит эту границу. Она не говорит <<вся топология построена без аксиом>> — это было бы неправдой о компактностном слое. Она говорит точнее: топологический слой конструктивен; компактностный слой опирается на законы логики ToS, и каждое такое обращение отмечается на месте.

О статусе аксиом: техническое и онтологическое

Здесь нужно условиться о словах, иначе вторая половина главы прозвучит тревожнее, чем следует.

Когда глава говорит, что доказательство <<использует аксиому classic>> или <<аксиому L4_witness>>, речь идёт о вполне определённых объектах из файла ToS_Axioms.v. Но эти объекты — не чужеродные костыли и не уступка нестрогости. Это технические Rocq-аксиомы, реализующие онтологические законы логики ToS. Аксиома classic — это $L 3$ , закон исключённого третьего, в той форме, в какой его принимает Rocq. Аксиома L4_witness — это $L 4$ , закон достаточного основания.

Разница принципиальна. В чисто конструктивной математике появление classic было бы признанием слабости — <<здесь не удалось построить, пришлось постулировать>>. В ToS это не так. $L 3$ и $L 4$ — законы логики ToS, принятые на уровне самой системы (Часть I). Когда доказательство <<использует classic>>, оно не отступает от строгости — оно явно учитывает, что опирается на закон логики ToS, а не выводится из одной лишь вычислительной конструктивности. Технические аксиомы Rocq — это ровно тот мост, по которому онтологические законы логики входят в формальную проверку.

Поэтому всякий раз, когда глава отмечает обращение к $L 3$ или $L 4$ , это не сигнал тревоги, а честный учёт уровня: данное рассуждение опирается на закон логики, и глава говорит, на какой именно. Различать <<доказано конструктивно>> и <<доказано с опорой на закон логики ToS>> — значит не прятать структуру доказательства, а показывать её.

Замысел главы

Глава идёт от простого к трудному. Сначала — открытые и замкнутые множества над $Q$ (§ 2.2) и процессный взгляд на открытое множество как на процесс покрытий (§ 2.3). Затем — отделимость: хаусдорфовость $Q$ (§ 2.4). Далее — центральный и самый ответственный раздел: компактность и неполнота $Q$ , теорема Гейне–Бореля (§ 2.5). Затем — тотальная ограниченность и $ε$ -сети, с вычислительным примером (§ 2.6). Затем — Больцано–Вейерштрасс, честно разобранный вместе с его аксиомным основанием (§ 2.7). И наконец — связность, унификация трёх лиц компактности и итог главы (§ 2.8).

Опорных файлов одиннадцать — шесть основных и пять вспомогательных process-обёрток; все сверены с репозиторием дословно. Топологический слой — без аксиом; компактностный — с явно учтёнными $L 3$ и $L 4$ .

Открытые и замкнутые множества над $Q$ {Q}

Открытый шар и открытое множество

Топология начинается с понятия окрестности. И простейшую окрестность мы уже умеем построить из материала Главы 5.1 — это открытый шар: множество всех точек, отстоящих от центра меньше чем на заданный радиус. Расстояние у нас есть — то самое рациональное $∣ x - c ∣$ ; шар определяется им сразу. В Rocq это записано в файле Topology.v так:

Definition open_ball (center radius : Q) (x : Q) : Prop :=
  Qabs (x - center) < radius.

Точка $x$ лежит в шаре с центром center и радиусом radius, если расстояние от $x$ до центра строго меньше радиуса. Всё над $Q$ : центр, радиус, точка — рациональные.

Из шара мы выращиваем центральное понятие топологии — открытое множество. Множество назовём открытым, если у каждой его точки есть запас свободного пространства: шар, целиком лежащий внутри множества. Где бы внутри $S$ ни находилась точка, вокруг неё есть <<воздух>> — шар, не выходящий за пределы $S$ . В Rocq:

Definition is_open (S : Q -> Prop) : Prop :=
  forall x, S x -> exists eps, 0 < eps /\
    forall y, open_ball x eps y -> S y.

Множество $S$ открыто, если у каждой его точки $x$ есть положительный радиус $ε$ такой, что весь шар $B (x, ε)$ целиком лежит в $S$ .

Замкнутое множество мы определяем через открытое — как дополнение к открытому: $S$ замкнуто, если множество точек вне $S$ открыто. В Rocq это прямая запись:

Definition is_closed (S : Q -> Prop) : Prop :=
  is_open (fun x => ~ S x).

И, наконец, ограниченным мы называем множество, целиком умещающееся в некоторый шар вокруг нуля.

Девятнадцать лемм топологии над Q

На этих определениях мы строим весь базовый аппарат точечно-множественной топологии над $Q$ — и строим конструктивно, ни разу не прибегая к аксиоме. Девятнадцать лемм Topology.v подтверждают каждый шаг; перечислим главные.

Шар открыт. Открытый шар сам есть открытое множество: у всякой его внутренней точки $y$ есть запас свободного пространства — шар радиуса $r - ∣ y - c ∣$ , который неравенством треугольника не выходит за пределы $B (c, r)$ . Это лемма open_ball_is_open.

Пустое и полное множества открыты. Два вырожденных, но необходимых случая: и пустое множество, и всё $Q$ открыты (empty_is_open, full_is_open).

{ Объединение и пересечение двух открытых открыты. Топология замкнута относительно двух базовых операций над множествами; для пересечения запас свободного пространства берётся как меньший из двух запасов. Это union_two_open и intersection_two_open. }

{ Интервалы. Открытый интервал $(a, b)$ есть открытое множество, замкнутый интервал $[a, b]$ — замкнутое (interval_open, closed_interval_closed). Эти два факта — опора всей будущей теории компактности: компактным окажется именно замкнутый интервал. }

{ Непрерывность. Здесь же мы вводим и непрерывность — в точке (continuous_at) и всюду (continuous) — и устанавливаем её устойчивость: тождество и постоянная непрерывны, сдвиг $x \mapsto x + c$ непрерывен, сумма, отрицание и композиция непрерывных функций непрерывны. И ключевую для топологии лемму — continuous_preserves_open_preimage: прообраз открытого множества под непрерывным отображением открыт. Это топологическое определение непрерывности в эквивалентной форме; к нему подробно вернётся Глава 5.3. }

Топология над Q, не над классами

Одно уточнение, важное для всей главы. Всё, что построено в Topology.v, — топология над рациональными числами. Открытое множество здесь есть предикат Q -> Prop — подмножество $Q$ ; непрерывность — свойство функций $Q \to Q$ .

Это не топология на фактор-классах RealPoint — на тех классах эквивалентных процессов, которыми Часть IV определяла точку. В опорных файлах этой главы топология живёт на уровне $Q$ . Но базис метрической топологии на классах уже перенесён — отдельным файлом RealPointTopology.v: там определён открытый шар на классах rp_in_ball (центр — точка, радиус — рациональное) и доказана его корректность на классах (rp_in_ball_well_defined: принадлежность шару не зависит от выбора представителя), а также rp_in_ball_centre (центр лежит в своём шаре). Полная же теория открытых и замкнутых множеств на классах — ещё не перенесена. Различать рациональный уровень и уровень классов глава будет последовательно: топология над $Q$ — прочный конструктивный фундамент; на классах построен её метрический базис (шар с корректностью), а полная топология классов — направление дальнейшей работы.

И заметим главное о топологическом слое: Topology.v — девятнадцать лемм, ноль аксиом. Открытые множества, замкнутые множества, непрерывность, интервалы — весь этот аппарат ToS получает чисто конструктивно, из одного рационального расстояния. Аксиомы появятся позже — когда глава дойдёт до компактности.

Разбор E/R/R: топология как система

Топология — система, а значит, к ней приложима методология E/R/R (Часть I): разбор на три аспекта — Elements, Roles, Rules. Проведём его. Как и для метрики в Главе 5.1, разбор не навязывает ничего извне — он разворачивает разметку, уже стоящую в заголовке опорного файла: элементы — точки, подмножества, шары; роли — точка как позиция, шар как окрестность, множество как область; правила — открытость и непрерывность как конституции.¹ Порядок разбора — онтологический, Rules $\to$ Roles $\to$ Elements; познавательно мы шли обратным путём — от шара и открытого множества к аксиомам, которым они подчинены.

Оговорка о статусе — та же, что в Главе 5.1. Топология здесь живёт над рациональными числами: открытое множество есть предикат Q -> Prop, непрерывность — свойство функций $Q \to Q$ (§ 2.2.3). Называя это системой, мы ведём содержательную онтологическую интерпретацию, а не приписываем коду объект типа System $L$ . Разбор читает структуру файла, не добавляя ему формального содержания.

Rules — правила, удерживающие топологию (закон $L 5$ : правила стоят над тем, что организуют). И здесь разбор проясняет главную тему главы — два слоя. Правила топологии расслаиваются. Универсальный слой — законы $L 1$ – $L 5$ . Конкретный конструктивный слой — две конституции из заголовка: открытость (<<у каждой точки множества есть шар внутри него>>) и непрерывность (<<прообраз открытого открыт>>), а с ними замкнутость топологии относительно объединения и пересечения и факты об интервалах — весь топологический аппарат § 2.2, доказанный без единой аксиомы. И — конкретный слой, опирающийся на законы логики — правила компактности: <<конечное подпокрытие существует>>, <<процесс построения терминирует>>. Как покажут § 2.5 и § 2.7, эти правила привлекают $L 3$ (а Больцано–Вейерштрасс — и $L 4$ ). Различие, проходящее через всю главу, — между конструктивной топологией и компактностью, обнаруживающей неполноту $Q$ , — есть, в терминах разбора, расслоение внутри Rules: одни правила конструктивны, другие явно учитывают закон логики ToS.

Roles — значимость позиций (закон $L 4$ : каждая роль структурно обоснована). Заголовок называет три роли: точка играет роль позиции, шар — окрестности, множество — области. Эти роли не произвольны: по $L 4$ их основание — в самих правилах (шар есть окрестность именно потому, что вокруг своей точки даёт <<запас свободного пространства>>; множество есть область потому, что открытость наделяет каждую его точку таким запасом). В процессном слое (§ 2.3) к ним добавляются роли покрытия и уточнения: конечные наборы шаров, накрывающие множество, и переход к более мелким наборам.

Elements — носители (закон $L 1$ и принцип $P 4$ ). Элементы — точки $Q$ , подмножества Q -> Prop и открытые шары. По $L 1$ каждая точка тождественна себе. А в процессной форме открытого множества (§ 2.3) носители — конечные рациональные покрытия: <<целое>> открытого множества потенциально, но всякий его кадр конечен и обозрим (лемма p4_cover_finite) — прямое проявление $P 4$ .

Сведём разбор в таблицу.

Компонент	Что фиксирует	E/R/R
точки $Q$ , подмножества, шары	носители	Element
точка $\to$ позиция, шар $\to$ окрестность, множество $\to$ область	ролевые позиции	Role
открытость, непрерывность	конституции	Rule (конструкт.)
замкнутость по $\cup$ / $\cap$ , интервалы	правила топологии	Rule (конструкт.)
конечное подпокрытие, терминация	компактность	Rule (опора на $L 3$ / $L 4$ )
законы $L 1$ – $L 5$	универсальный слой	Rule (универс.)

Хорошая сформированность. Разметка однозначна: точки и шары суть элементы, позиция/окрестность/область — роли, открытость и непрерывность — правила; ни один компонент не претендует на две категории. Самореференции нет: критерий открытости квантифицирует по точкам множества и стоит над ними — по $L 5$ операция выше своих операндов. Топология хорошо сформирована.

Разбор объясняет уже сделанные в главе различения. Двухслойность, о которой § 2.1 говорит как о главном уроке, оказывается расслоением Rules: топологические конституции конструктивны, компактностные правила опираются на законы логики. Хаусдорфовость (§ 2.4) — правило, которым топология уважает акт различения: различимые элементы оказываются и пространственно отделимы. А <<три лица компактности>> (§ 2.8) — Гейне–Борель, нётеровость, терминация процесса — суть одно Rule-уровневое свойство, прочитанное под $P 4$ как простейший, завершающийся за конечное число шагов процесс. И тот же разбор задаёт образец: каждое топологическое понятие Часть V читает как процессный паттерн со своей E/R/R-структурой.

Открытое множество как процесс покрытий

Процессный взгляд

До сих пор открытое множество было у нас предикатом — $S : Q \to P r o p$ . Это статичное описание: про каждую точку сказано, внутри она или нет. Но вся ToS приучила смотреть иначе — и открытое множество естественно переосмыслить процессно.

Рассуждение здесь то же, что превращало число в процесс приближений (Часть IV). Под $P 4$ открытое множество не может быть завершённым подмножеством $R$ — завершённого $R$ нет. Зато его можно предъявлять: процессом рациональных покрытий шарами, последовательностью всё более подробных конечных наборов рациональных шаров. Такой процесс — это процессное представление открытости: способ показать, как открытое множество разворачивается конечными приближениями, уровень за уровнем. Объект, который классическая математика мыслит готовым, ToS видит разворачивающейся последовательностью конечных приближений; этот же ход мы и применяем к открытому множеству. В Rocq процессный слой собран в файле ProcessTopOpen.v.

Шар, покрытие, процесс

Строим этот взгляд снизу вверх. В основании — рациональный шар: in_ball c r x означает $∣ x - c ∣ < r$ , та же конструкция, что в § 2.2. Его базовые свойства те же: центр лежит в своём шаре, и — in_ball_shrink — если точка внутри шара, вокруг неё помещается меньший шар (снова неравенство треугольника).

Над шаром — открытое множество в процессной форме, is_open_process, и тот же набор лемм, что в § 2.2, только на процессном языке: пустое и полное множества открыты, шар открыт (ball_is_open), объединение и пересечение открытых открыты, открытый интервал открыт.

И на вершине — собственно покрытие и процесс покрытий, которые и несут процессную идею:

Definition QBallCover := list (Q * Q).
 
Definition OpenProcess := nat -> QBallCover.
 
Definition is_refining (op : OpenProcess) : Prop :=
  forall n x, covered_by_balls (op n) x ->
              covered_by_balls (op (S n)) x.

QBallCover — конечный список пар <<центр, радиус>>: конечный набор рациональных шаров. OpenProcess — функция из номера уровня в такой набор: на каждом уровне — своё конечное покрытие. is_refining — свойство уточнения: всё, что покрыто на уровне $n$ , остаётся покрытым на уровне $n + 1$ . Покрытие с уровнями не теряет точек, только добавляет.

Существенно, что на каждом уровне покрытие конечно — список конечной длины; это устанавливает лемма p4_cover_finite. И здесь прямо виден $P 4$ : открытое множество разворачивается как бесконечный процесс, но всякий его кадр — конечный, обозримый набор шаров. <<Целое>> открытого множества потенциально, <<кадр>> — актуально конечен.

Что даёт процессный взгляд

Зачем процессная форма, если Topology.v уже дал открытое множество предикатом? Затем же, зачем Часть IV давала число процессом. Предикат $S : Q \to P r o p$ описывает результат — но не путь к нему. Процесс покрытий описывает, как открытое множество строится: уровень за уровнем, конечным набором шаров за конечным набором. Для онтологии ToS это не стилистическая деталь, а суть: открытое множество — не данная разом область, а процесс её рационального исчерпания.

Будем, однако, точны в том, что именно мы здесь построили, а что — нет. Построена инфраструктура: QBallCover, OpenProcess, is_refining, covered_by_balls — и доказаны её базовые свойства. Чего мы не доказали — так это полной теоремы эквивалентности: что всякому открытому предикату $S : Q \to P r o p$ отвечает процесс покрытий, исчерпывающий ровно $S$ , и наоборот. Поэтому процесс покрытий честно назвать процессным представлением открытости, инфраструктурным слоем — а не доказанным тождеством между всеми открытыми предикатами и процессами покрытий. Глава так им и пользуется: как способом предъявить открытость конечными приближениями, не как теоремой о совпадении двух описаний. То, что в ProcessTopOpen.v построено, мы выдаём ровно за то, что оно есть.

{ И — важное для общей картины главы: процессный слой, как и топологический, остаётся конструктивным — ProcessTopOpen.v, подобно Topology.v, не использует ни одной аксиомы. }

Отделимость: $Q$ хаусдорфово{Отделимость: Q хаусдорфово}

Различить — значит отделить

Вся ToS выросла из единственного акта — акта различения. Различить два объекта — исходный шаг, с которого начинается всё остальное. У этого акта есть топологическое лицо, и оно называется хаусдорфовостью.

Топологическое пространство хаусдорфово, если любые две различные точки можно отделить — поместить в непересекающиеся окрестности. Различить две точки логически (сказать: они не равны) и различить их топологически (развести в непересекающиеся шары) — в хаусдорфовом пространстве это одно и то же. Хаусдорфовость есть утверждение, что логическое различение поддержано пространственно.

Теорема hausdorff_Q

Установим, что $Q$ хаусдорфово — и проследим, как это выводится. Дано: две различные рациональные точки $x$ и $y$ . Нужно: развести их в непересекающиеся шары.

Рассуждение прямое. Раз $x \neq = y$ , расстояние между ними положительно — это отдельный факт, лемма not_Qeq_pos_dist: различные рациональные числа имеют строго положительное расстояние. Возьмём радиус $e$ равным половине этого расстояния. Если бы некоторая точка $z$ попала в оба шара радиуса $e$ сразу — вокруг $x$ и вокруг $y$ , — то по неравенству треугольника расстояние от $x$ до $y$ оказалось бы меньше $e + e$ , то есть меньше самого расстояния от $x$ до $y$ . Это невозможно; значит, общих точек у шаров нет, и точки отделены. Так выводится теорема hausdorff_Q, записанная в ProcessTopOpen.v так:

Theorem hausdorff_Q : forall x y : Q,
  ~ (x == y) ->
  exists e : Q, 0 < e /\
    (forall z, Qabs (z - x) < e -> Qabs (z - y) < e -> False).

Для любых двух различных рациональных $x$ и $y$ существует положительный радиус $e$ такой, что ни одна точка $z$ не лежит одновременно в шаре радиуса $e$ вокруг $x$ и в шаре радиуса $e$ вокруг $y$ , — ровно то, что мы и вывели.

Хаусдорфовость и акт различения

Стоит задержаться на том, почему эта простая теорема важна онтологически.

ToS начинается с акта различения: $A = \exists$ , и различить — значит положить границу. Лемма not_Qeq_pos_dist — буквальное воплощение этого на уровне рациональных чисел: если два числа различены (не равны), то между ними есть зазор — положительное расстояние. Различение не бывает <<бесконечно малым>>: оно либо есть, и тогда есть измеримый зазор, либо его нет вовсе.

Хаусдорфовость надстраивает над этим топологический этаж. Положительный зазор между точками означает, что вокруг каждой можно очертить окрестность — и эти окрестности не сольются. Логическое различение ( $x \neq = y$ ) разворачивается в пространственное разделение (непересекающиеся шары). Хаусдорфовость — это гарантия, что топология $Q$ уважает исходный акт различения: то, что различено, может быть и разделено. В терминах разбора § 2.2.4 отделимость — правило (Rule), которым топология уважает различимость элементов.

И — по-прежнему — ни одной аксиомы. hausdorff_Q и not_Qeq_pos_dist доказаны чисто конструктивно. Весь топологический слой — открытые множества, замкнутые множества, непрерывность, отделимость — ToS строит без обращения к законам логики. Это меняется в следующем разделе, где глава доходит до компактности.

Компактность: где $Q$ обнаруживает неполноту{Компактность: где Q обнаруживает неполноту}

Жирная черта

Это центральный и самый ответственный раздел главы, и начать его надо прямым тезисом.

Классическая теорема Гейне–Бореля над $Q$ неверна. И это не дефект формализации, а математический факт.

Классический Гейне–Борель утверждает: всякое открытое покрытие замкнутого ограниченного интервала имеет конечное подпокрытие. Над действительными числами это верно. Над рациональными — нет. Глава не прячет этот разрыв и не выдаёт желаемое за доказанное: она показывает, где проходит граница и как ToS с ней работает.

Контрпример

{ Почему классический Гейне–Борель над $Q$ ложен — видно из контрпримера. Файл HeineBorel_ERR.v фиксирует общий смысл препятствия — классический Гейне–Борель требует полноты, которой у $Q$ нет, — а конкретную конструкцию мы приведём здесь как пояснение главы. }

Возьмём иррациональное число $α$ , лежащее внутри интервала — скажем, $α = 2 /2$ на отрезке $[0, 1]$ . Для каждой рациональной точки $x$ интервала зададим радиус

C (x) = \frac{1}{2} ∣ x - α ∣.

Этот радиус строго положителен: $x$ рационально, $α$ иррационально, совпасть они не могут. Значит, покрытие корректно — каждая рациональная точка $x$ накрывается хотя бы своим собственным шаром.

Но конечного подпокрытия у этого покрытия нет. Пусть выбран конечный набор центров $x_{1}, \dots, x_{k}$ . Величина

d = i min ∣ x_{i} - α ∣

строго положительна — минимум конечного набора положительных чисел. Шар вокруг центра $x_{i}$ имеет радиус $\frac{1}{2} ∣ x_{i} - α ∣$ и потому не дотягивается до $α$ ближе чем на $\frac{1}{2} ∣ x_{i} - α ∣ \geq \frac{1}{2} d$ : всякая точка, отстоящая от $α$ меньше чем на $\frac{1}{2} d$ , не покрыта ни одним из выбранных шаров. Рациональные точки в этой окрестности $α$ есть — по плотности $Q$ , — и ни один из конечного числа шаров их не накрывает. Конечный набор центров не покрывает весь рациональный интервал.²

Существенно, что именно ломает компактность. Зазор у $α$ — иррациональной точки, которой в $Q$ нет и которая в покрываемом множестве не участвует, — и есть та <<дыра>>, сквозь которую утекает конечность подпокрытия. Шары мельчают по мере приближения к $α$ , и половинный радиус не даёт им сомкнуться над зазором.

Корень в одном слове — неполнота. Классическое доказательство Гейне–Бореля опирается на полноту: вложенные интервалы сходятся к точке, и эта точка обязана существовать. Над $Q$ она не обязана: вложенные интервалы могут сходиться к иррациональному зазору. Компактность — ровно то место, где $Q$ обнаруживает свою неполноту, о которой Глава 5.1 говорила как о понятии. Здесь это понятие становится осязаемым препятствием.

Ремонт: число Лебега

Сломанную теорему мы не оставляем сломанной — мы её ремонтируем. Контрпример указал, что именно ломает компактность: радиусы покрытия могут стремиться к нулю у иррационального зазора. Значит, ремонт — добавить к покрытию условие, которое этой патологии не допускает: запретить радиусам выдыхаться. Такое условие — равномерность покрытия, или, в классических терминах, наличие числа Лебега. В Rocq оно записано так:

Definition uniform_cover (C : OpenCover) (a b delta : Q) : Prop :=
  delta > 0 /\ forall x : Q, a <= x <= b -> C x >= delta.

Обычное покрытие (valid_cover) лишь требует, чтобы у каждой точки радиус был положителен, — и этого, как показал контрпример, мало. uniform_cover требует большего: существует единый положительный $δ$ , не превосходимый снизу ни одним радиусом. Радиусы не могут <<выдохнуться>> — у всех есть общая нижняя граница. Это и есть число Лебега: масштаб, на котором покрытие работает равномерно по всему интервалу.

С этим условием Гейне–Борель снова доказуем. Рассуждение — бисекция: делим интервал пополам, каждую половину — снова пополам. Поскольку все радиусы не меньше $δ$ , дробление можно остановить, как только ширина куска станет меньше $δ$ : такой кусок целиком накрывается одним шаром. Архимедовость $Q$ гарантирует, что нужная мелкость достигается за конечное число шагов, — и конечное подпокрытие собирается из конечного числа шаров. Этот вывод формализован в HeineBorel_ERR.v (бисекционный спуск — hb_step, Qpow2, Heine_Borel_by_depth) и собран в теорему:

Theorem Heine_Borel_uniform : forall (C : OpenCover) (a b delta : Q),
  a < b ->
  uniform_cover C a b delta ->
  exists centers : FiniteSubcover, covers_interval C centers a b.

При наличии числа Лебега конечное подпокрытие существует. Теорема Heine_Borel — то же утверждение с явно вынесенной гипотезой существования числа Лебега.

Что доказано и что нет

{ Будем точны в том, что именно установлено. Доказана равномерная версия Гейне–Бореля — для покрытий, обладающих числом Лебега. Полная классическая компактность — <<всякое покрытие имеет конечное подпокрытие>>, без оговорки о равномерности, — не доказана, и доказана быть не может: ей противоречит контрпример. Глава не выдаёт Heine_Borel_uniform за классическую теорему. Это честный ремонт: теорема восстановлена на том классе покрытий, на котором она вообще верна над $Q$ . }

Аксиомный статус: $L 3$ {L3} в бисекции

{ И — по уговору § 2.1 — честно отметим, где наше рассуждение опирается на закон логики. Бисекция Гейне–Бореля держится на одном шаге, который конструктивным не является. Шаг этот — лемма not_coverable_half: если интервал не покрывается конечным числом шаров, то и одна из его половин не покрывается. Утверждение верное — но чтобы указать, какая именно половина не покрывается, нужен закон исключённого третьего. Поэтому HeineBorel_ERR.v импортирует ToS_Axioms.v и эта лемма пользуется classic. }

Вспомним уговор § 2.1: classic — это техническая Rocq-реализация $L 3$ , закона исключённого третьего ToS. Обращение к ней — не брешь в строгости, а явный учёт уровня: бисекционный аргумент Гейне–Бореля опирается на закон логики ToS, и глава это отмечает. Компактностный слой при этом неоднороден. Одни его части вполне конструктивны — например, тотальная ограниченность интервала и построение $ε$ -сетей, к которым глава перейдёт в § 2.6. Другие — например, бисекционные рассуждения о непокрываемой или о бесконечно населённой половине — опираются на $L 3$ . Различать <<доказано конструктивно>> и <<доказано с опорой на $L 3$ >> здесь не педантизм, а точное описание того, на чём стоит каждая конкретная теорема. Это и есть тот опирающийся на закон логики подслой Rules, который выделил разбор § 2.2.4.

Тотальная ограниченность и $ε$ -сети{Тотальная ограниченность и eps-сети}

Другой подход к компактности

Раздел 2.5 показал, что классический Гейне–Борель над $Q$ ломается, и отремонтировал его условием числа Лебега. Зайдём теперь с другой стороны: часть того же разрыва можно закрыть иным понятием — тотальной ограниченностью, — и это понятие над $Q$ ведёт себя гораздо смирнее.

Идея проста. Вместо того чтобы говорить о покрытиях произвольными шарами, потребуем малого: чтобы всё множество можно было приблизить конечной сеткой точек с любой наперёд заданной точностью. Такая сетка называется $ε$ -сетью, а свойство интервала иметь $ε$ -сеть для каждого $ε$ — тотальной ограниченностью. В Rocq (файл HeineBorelComplete.v) это записано так:

Definition eps_net (pts : list Q) (a b eps : Q) : Prop :=
  forall x : Q, a <= x <= b ->
    exists p : Q, In p pts /\ Qabs (x - p) < eps.
 
Definition totally_bounded (a b : Q) : Prop :=
  forall eps : Q, eps > 0 ->
    exists pts : list Q, eps_net pts a b eps.

eps_net — конечный список точек pts такой, что всякая точка интервала отстоит от какой-нибудь точки списка меньше чем на $ε$ . totally_bounded — свойство интервала иметь такую сеть для каждого $ε$ : как бы мелко ни требовалась точность, конечная сетка, накрывающая всё с этой точностью, найдётся.

Главная теорема: интервал тотально ограничен

{ Установим главное: всякий замкнутый интервал тотально ограничен. В HeineBorelComplete.v это теорема: }

Theorem totally_bounded_interval : forall a b,
  a <= b -> totally_bounded a b.

И — что важно для онтологии ToS — доказывается она конструктивно, прямым построением сетки. По заданному $ε$ раскладываем по интервалу равномерный рациональный грид с шагом, вычисляемым из $ε$ , и предъявляем его как конечный список точек; всякая точка интервала оказывается ближе $ε$ к какому-нибудь узлу грида. Никакого обращения к законам логики — сетка строится явно (лемма rational_eps_net, узлы — grid_points).

В отличие от Гейне–Бореля, где над $Q$ возникла настоящая трудность, тотальная ограниченность интервала — результат конструктивный и беспроблемный. И это понятно: тотальная ограниченность не требует, чтобы предельная точка существовала, — она требует лишь, чтобы интервал можно было приблизить конечной сеткой. А приближать конечным $Q$ умеет без всякой полноты.

{ На том же фундаменте мы строим и мост к равномерной непрерывности — задел для Главы 5.3. Липшицево отображение равномерно непрерывно (lipschitz_uniform_cont); это конструктивная замена недоказуемой над $Q$ классической импликации <<непрерывность влечёт равномерную непрерывность>>. Сумма, масштаб и композиция равномерно непрерывных функций снова равномерно непрерывны. Весь этот аппарат HeineBorelComplete.v подаёт Главе 5.3. }

Оговорка об аксиомном статусе

{ Здесь нужна честная оговорка — и она же иллюстрирует общее правило аудита ToS. Заголовок файла HeineBorelComplete.v объявляет статус <<0 axioms>>. Но это статус файла по заголовку, а не каждой теоремы в нём. Среди лемм файла есть mono_bounded_is_cauchy — <<монотонная ограниченная последовательность есть Коши>>, — и она использует classic (через приём NNPP, снятие двойного отрицания). }

{ Противоречия с заголовком нет — есть напоминание о правиле, заведённом ещё в Главе 4.6: аксиомный статус проверяется по конкретной теореме, командой Print Assumptions, а не приписывается файлу оптом. totally_bounded_interval и построение $ε$ -сетей — конструктивны. А mono_bounded_is_cauchy опирается на $L 3$ — и, по уговору § 2.1, это явный учёт уровня: данная лемма стоит на законе исключённого третьего ToS, и аудит это фиксирует. }

Вычислительный пример: сетка интервала

Тотальная ограниченность — понятие, которое легко сделать осязаемым. Это третий, вычислительный слой изложения. Возьмём интервал $[0, 1]$ и посчитаем, сколько точек нужно в $ε$ -сетке для нескольких уровней точности.

Грид раскладывается с шагом, равным $ε$ ; число точек — это число шагов длины $ε$ , укладывающихся в единичный интервал, плюс одна. Вот результат:

Точность $ε$	Шаг сетки	Довольно точек для $[0, 1]$
$1/4$	$1/4$	$5$
$1/8$	$1/8$	$9$
$1/16$	$1/16$	$17$

{

Прочтём таблицу. Чтобы накрыть $[0, 1]$ с точностью $1/4$ , довольно пяти точек — $0, 1/4, 1/2, 3/4, 1$ : всякая точка интервала отстоит от какой-нибудь из них меньше чем на $1/4$ . С точностью $1/8$ — девяти точек. С точностью $1/16$ — семнадцати. Сетка конечна при каждом $ε$ , и её размер прямо вычисляется: при уменьшении $ε$ вдвое число точек примерно удваивается. Это и есть тотальная ограниченность в работе: не отвлечённое <<сетка существует>>, а конкретная конечная таблица. И всё вычислимо — никакой полноты, никакого предельного перехода, только рациональная арифметика. }

Одна техническая оговорка. Таблица выше — минимально интуитивная сетка с шагом ровно $ε$ . Формальное доказательство в HeineBorelComplete.v устроено надёжнее: лемма rational_eps_net строит грид с половинным шагом $ε /2$ , чтобы гарантировать строгое неравенство $∣ x - p ∣ < ε$ без оговорок о крайних точках. Таблица здесь — педагогическая иллюстрация порядка величин, а не буквальный grid_points из доказательства; код берёт вдвое более частую сетку и тем избавляется от возни с границами.

Больцано–Вейерштрасс: компактность через бисекцию

Вторая теорема компактности

Гейне–Борель говорит о покрытиях. У компактности есть и второе лицо, двойственное первому, — теорема Больцано–Вейерштрасса, говорящая о последовательностях. Классически её формулируют как существование сходящейся подпоследовательности у всякой ограниченной последовательности. Текущая формализация доказывает близкую, Коши-совместимую форму. В терминах ToS, где предел — это процесс: всякая ограниченная последовательность рациональных чисел имеет точку сгущения — процесс Коши, к которому члены последовательности с большими индексами сколь угодно приближаются. Именно эта — через точку сгущения, а не через явно построенную подпоследовательность $k : N \to N$ , — формулировка и будет доказана.

{ Доказать эту теорему — наш следующий шаг (формализация её собрана в BolzanoWeierstrass.v). И сразу — честно, по уговору § 2.1 — об основании, на котором она будет стоять. В отличие от тотальной ограниченности § 2.6, Больцано–Вейерштрасс конструктивным не будет: его доказательство опирается на два закона логики ToS — $L 3$ и $L 4$ . Заголовок BolzanoWeierstrass.v аксиомного статуса не скрывает и объявляет его прямо: <<Axioms: classic ( $L 3$ ), L4_witness ( $L 4$ )>>. Глава делает это основание не примечанием мелким шрифтом, а узлом раздела — и § 2.7.2 покажет в точности, где и почему законы логики вступают в дело. }

Бисекция и выбор половины

Доказательство — бисекция, родственная той, что работала в Гейне–Бореле, но применённая к последовательности. Дан интервал $[a, b]$ , в котором лежит ограниченная последовательность $s$ . Делим интервал пополам. В одной из половин — по крайней мере в одной — лежит бесконечно много членов последовательности (всех членов бесконечно много, а половин две). Выбираем такую половину, снова делим, и так далее. Получается процесс вложенных интервалов, чья ширина стремится к нулю; <<точка>>, к которой они стягиваются, — и есть точка сгущения.

{ В этом рассуждении есть в точности один неконструктивный шаг — и мы его не маскируем, а указываем прямо. Шаг — выбор половины; в Rocq он записан так: }

Definition bw_step (s : nat -> Q) (st : BWState) : BWState.
Proof.
  destruct (L3_informative (bw_step_left s st)) as [H | H].
  - exact (mkBW (bw_left st) (bw_mid st)).
  - exact (mkBW (bw_mid st) (bw_right st)).
Defined.

Чтобы выбрать, идти в левую половину или в правую, нужно решить, в левой ли половине бесконечно много членов. А этого — в общем случае — конструктивно решить нельзя: проверка <<бесконечно много>> не завершается за конечное время. Здесь и вступает L3_ informative — информативная форма закона исключённого третьего: она постановляет, что одна из двух возможностей имеет место, и позволяет разобрать случаи. Лемма infinite_pigeonhole — бесконечный вариант принципа Дирихле, <<хотя бы в одной половине бесконечно много>>, — по той же причине использует classic.

По уговору § 2.1: L3_informative и classic — технические Rocq-реализации $L 3$ . Выбор половины опирается на закон исключённого третьего ToS. Это не изъян доказательства — это его честно предъявленная структура. Бисекция Больцано–Вейерштрасса по своей природе неконструктивна: <<населённую>> половину нельзя вычислить, её можно лишь назвать по $L 3$ . ToS принимает $L 3$ как закон логики — и потому теорема в ToS доказуема; но доказуема именно с опорой на закон логики, а не из чистого вычисления, и глава говорит об этом прямо.

Уточним и характер этого шага. bw_step выбирает половину классическим разбором случаев по предложению <<в левой половине бесконечно много членов>> — через L3_informative. Это не полноценный алгоритм построения подпоследовательности по индексам и не выбор минимального индекса. Бисекция Больцано– Вейерштрасса — это процесс построения вложенных интервалов и Коши-точки сгущения; неконструктивность сосредоточена ровно в одном месте — в удержании статуса <<населённой половины>> через разбор случаев, — и больше нигде.

Главная теорема

Остальные свойства бисекции конструктивны и отработаны подробно: каждый шаг сохраняет вложенность и <<населённость>> выбранной половины, ширина после $n$ шагов не превосходит $(b - a) / 2^{n}$ и — через архимедовость (bw_width_to_zero) — стремится к нулю, а левые и правые концы образуют процессы Коши. Собрав выбор половины с этими свойствами, получаем главную теорему — в BolzanoWeierstrass.v она записана так:

Theorem bolzano_weierstrass : forall (s : nat -> Q) (a b : Q),
  a < b -> bounded_seq s a b ->
  exists L : CauchySeq, is_cluster_point s L.

Всякая ограниченная последовательность в $[a, b]$ имеет точку сгущения — и эта точка предъявлена как CauchySeq, процесс Коши. Предикат is_cluster_point определён Коши-совместимо: для любой точности и любого порога найдётся член последовательности с большим индексом, лежащий к точке сгущения ближе требуемого. Двойственная пара теорем — monotone_bounded_cauchy и decreasing_bounded_cauchy — добавляет: монотонная ограниченная последовательность сама есть Коши.

Бисекция как процесс

{ Остаётся перевести результат на процессный язык ToS — эту обёртку несёт файл ProcessBW.v. Левые и правые концы бисекции мы рассматриваем как процессы над $Q$ (bw_left_process и bw_right_process) и устанавливаем: они монотонны (левые растут, правые убывают), оба суть Коши и сходятся к одному пределу. Теорема bw_is_process_construction собирает это в единую картину E/R/R, а bw_convergence_rate фиксирует скорость — $1/2$ : интервал на каждом шаге уполовинивается. }

{ Аксиомного основания процессная обёртка не меняет: она ничего не добавляет и не убавляет, перенося на язык процессов теорему, как она есть — доказанную, с опорой на $L 3$ и $L 4$ . Заголовок ProcessBW.v это и фиксирует: <<classic (inherited from BolzanoWeierstrass)>>. }

Онтологически бисекция Больцано–Вейерштрасса — чистый образец процесса ToS. Точка сгущения не дана заранее; она строится — шаг за шагом, делением за делением, выбором населённой половины за выбором. Результат — процесс Коши, разворачивающийся с темпом $1/2$ . То, что в классической математике есть готовая <<предельная точка>>, здесь — процесс; и единственное место, где процесс опирается не на вычисление, а на закон логики, — честно названный выбор половины.

Связность, унификация и итог главы

Связность: топологическая связность и процессные пути

Остаётся последнее топологическое понятие — связность. И с ним $Q$ ведёт себя поучительно: ответ зависит от того, какую связность спросить.

В смысле классической топологической связности $Q$ не связно — более того, вполне несвязно. Между любыми двумя рациональными числами лежит иррациональный зазор, по которому $Q$ можно рассечь надвое. Топологически рациональная прямая рассыпается в пыль; нетривиальных связных подмножеств у $Q$ нет.

Но есть и другое понятие перехода — и тут нужна терминологическая аккуратность, иначе возникнет конфликт со стандартной топологией. Если связности как цельности у $Q$ нет, спросим о связности как достижимости: можно ли пройти из одной рациональной точки в другую, не покидая множества? Для этого построим рациональную линейную интерполяцию — прямую параметризацию из $a$ в $b$ :

Definition linear_path (a b t : Q) : Q := a + t * (b - a).

linear_path — при параметре $t = 0$ даёт $a$ , при $t = 1$ — $b$ , между — линейную интерполяцию. <<Путь в множестве>> мы определяем так:

Definition PathIn (S : Q -> Prop) (gamma : Q -> Q) (a b : Q) : Prop :=
  gamma 0 == a /\ gamma 1 == b /\
  forall t, 0 <= t -> t <= 1 -> S (gamma t).

И вот здесь — существенная оговорка, которую глава делает прямо. В определении PathIn нет требования непрерывности отображения gamma. Стандартный топологический путь — это непрерывное отображение связного отрезка; именно непрерывность гарантирует, что образ связен. PathIn требует лишь, чтобы параметризация в концах попадала в $a$ и $b$ , а на всяком рациональном параметре оставалась внутри $S$ . Это не стандартная путь-связность — и мы не выдаём её за таковую. Это процессная путь-достижимость: рациональная параметризация, переводящая одну точку в другую, не покидая множества. В Rocq этот слой собран в ProcessTopConnected.v.

Поэтому глава не называет $Q$ <<путь-связным>> в топологическом смысле — это было бы неверно. Глава говорит точнее: $Q$ процессно достижимо. Что при этом установлено: linear_path остаётся внутри интервала, липшицева по $t$ , пути обращаются и склеиваются; interval_path_connected даёт процессную достижимость для замкнутого интервала; процессная форма process_path — ходок, движущийся из $a$ к $b$ , на шаге $n$ занимающий параметр $t = n / (n + 1)$ , и process_path_cauchy показывает, что этот процесс есть Коши и сходится к $b$ . Весь этот слой — ноль аксиом.

Различие двух понятий онтологически важно. Топологическая связность спрашивает о завершённом континууме без дыр — и $Q$ его не образует. Процессная достижимость спрашивает о процессе перехода — и процесс линейной интерполяции $Q$ строит без труда. То, что для классической топологии есть недостаток $Q$ (вполне несвязность), для процессной онтологии ToS оказывается несущественно: важна не статичная цельность, а возможность пройти — а пройти из точки в точку рациональный процессный путь позволяет. В терминах E/R/R-разбора (§ 2.2.4) достижимость — это роль (Role): процессный путь, ведущий от одной точки к другой.

Три лица компактности

Сведём теперь вместе разные облики компактности — их в ToS оказывается три, и они суть одно. Под $P 4$ компактность — простейший случай процесса: процесс, который терминирует, завершается за конечное число шагов. У этого простейшего случая три имени.

Гейне–Борель: всякое (равномерное) покрытие имеет конечное подпокрытие. Нётеровость: всякая ограниченная возрастающая цепь стабилизируется. Терминация: процесс построения завершается за конечное число шагов. Три формулировки об одном; в ProcessTopCompact.v их единство закреплено теоремой p4_compactness_summary, а compact_eq_noetherian и compact_eq_hb связывают их попарно.

Стоит, однако, точно сказать о статусе этих сводных теорем. p4_compactness_summary и родственные ей — не новые результаты, а конъюнкции уже доказанного: они собирают вместе теоремы, установленные в HeineBorel_ERR.v и в файлах о нётеровости. То же относится к файлу ProcessTopUnified.v — сводке всего топологического материала: он перечисляет пять подпаттернов топологии (открытые множества, метрика, компактность, связность, отделимость) и помещает топологию одиннадцатым в ряду процессных паттернов ToS. ProcessTopUnified.v — обзорный файл, сводка; глава ссылается на него как на карту уже пройденного, не как на источник новых доказательств. И — по уговору § 2.1 — шапки ProcessTopCompact.v и ProcessTopUnified.v честно отмечают: classic унаследован от слоя нётеровости.

{ Сюда же относится и маленький файл ProcessCompactness.v с его теоремой compactness_foundation. Имя громкое — но, как и у process_space_complete в Главе 5.1, по своему содержанию это foundation-заготовка, а не теория компактности: она фиксирует базовые факты вроде ограниченности постоянного процесса и Коши-свойства постоянной последовательности. Глава учитывает её именно так и называет вещи своими именами. }

Что построено и что готовится

Итог главы — тремя списками, по дисциплине honest-режима.

Построено и проверено.

{ Топологический слой над $Q$ — открытые и замкнутые множества, шары, интервалы, непрерывность, хаусдорфовость, процессная путь-достижимость; конструктивно, без аксиом (Topology.v, ProcessTopOpen.v, ProcessTopConnected.v).}
Открытое множество в процессной форме — процесс конечных рациональных покрытий шарами, с уточнением по уровням.
Гейне–Борель в равномерной версии (Heine_Borel_ uniform) — для покрытий с числом Лебега; доказан бисекцией.
Тотальная ограниченность всякого интервала (totally_bounded_interval) — конструктивно, через явное построение $ε$ -сеток.
Больцано–Вейерштрасс (bolzano_weierstrass) — в CauchySeq-форме: всякая ограниченная последовательность имеет Коши-точку сгущения (а не явно построенную подпоследовательность).

На чём это стоит.

Топологический слой — на чистой конструкции, без законов логики.
Компактностный слой — на законах логики ToS: бисекция Гейне–Бореля и Больцано–Вейерштрасса опирается на $L 3$ (classic, L3_informative), Больцано–Вейерштрасс дополнительно — на $L 4$ (L4_witness). Это не изъян, а явный учёт уровня: технические Rocq-аксиомы реализуют онтологические законы логики ToS.

Не построено в этой главе.

Классический Гейне–Борель без оговорки о равномерности — он над $Q$ ложен, и это математический факт, а не пробел.
{ Полная топология открытых множеств и компактность на фактор-классах RealPoint — отдельной структурой не строятся; материал этой главы живёт на уровне $Q$ и процессов над $Q$ . (Базис метрической топологии на классах — открытый шар rp_in_ball с корректностью — построен отдельно, в RealPointTopology.v; см. § 2.2.3.)}

Готовит дальше. Равномерная непрерывность, Липшицев аппарат, $ε$ -сети — задел для Главы 5.3 о непрерывности; компактность интервала — инструмент, на котором будут стоять теоремы о промежуточном значении и об экстремуме.

Итог главы

Глава 5.2 прошла топологию процессов от открытого шара до точки сгущения. Её главный урок — о двух слоях. Топология как таковая — открытость, замкнутость, отделимость, связность — даётся ToS даром, чисто конструктивно, из одного рационального расстояния. Компактность — даётся иначе: здесь $Q$ обнаруживает неполноту, классический Гейне–Борель ломается, и теоремы восстанавливаются либо ремонтом (число Лебега), либо опорой на законы логики ToS. И эта опора — не слабость, а честно предъявленная структура: $L 3$ и $L 4$ суть законы логики ToS, и обращение к ним аудит отмечает не как брешь, а как учёт уровня.

{Итог главы — в трёх частях. Первое: что построено. Топологический слой над $Q$ — открытые и замкнутые множества, шары, интервалы, непрерывность, хаусдорфовость, процессная путь-достижимость — построен конструктивно, без единой аксиомы. Открытое множество получило процессную форму — процесс конечных рациональных покрытий шарами. Доказаны равномерная версия Гейне–Бореля, тотальная ограниченность всякого интервала и теорема Больцано–Вейерштрасса.}

{Второе: на чём это стоит. Топологический слой — на чистой конструкции. Компактностный слой — на законах логики ToS: бисекция Гейне–Бореля и Больцано–Вейерштрасса опирается на $L 3$ , Больцано–Вейерштрасс дополнительно на $L 4$ . Технические Rocq-аксиомы classic и L4_witness — это реализации онтологических законов логики ToS; обращение к ним есть явный учёт уровня доказательства, а не отступление от строгости.}

{Третье: что остаётся открытым. Классический Гейне–Борель без оговорки о равномерности над $Q$ неверен — это математический факт. На фактор-классах RealPoint построен базис метрической топологии — открытый шар rp_in_ball с корректностью (RealPointTopology.v, § 2.2.3); полная же теория открытых множеств и компактность на классах отдельной структурой не построены. Глава дала топологию процессов и две теоремы компактности; непрерывность, что встанет на этом основании, — предмет следующей главы Части V.}

Часть: Часть V. Топология и анализ процессов · Том: «Математика»

Понятия: Логика · Формализация

Навигация: ← Глава 1. Метрика на процессах · Глава 3. Непрерывность →

Дословная E/R/R-разметка в шапке файла Topology.v; здесь она разворачивается по образцу Части I. ↩
Эта конкретная конструкция теперь и машинно проверена — как самостоятельная 0-аксиомная теорема, а не только общий смысл препятствия. Для $[1, 2] \cap Q$ задано явное открытое покрытие $U_{k} = {x : ∣ x^{2} - 2∣ > 1/ (k + 1)}$ : оно накрывает весь рациональный отрезок (covers, ибо $x^{2} \neq = 2$ ), но конечного подпокрытия не имеет (no_finite_subcover) — у разреза $2$ величина $∣ x^{2} - 2∣$ убывает к нулю быстрее любого конечного порога. Вместе — Q_interval_not_compact; свидетелем служат Pell-приближения $2$ . Машинно проверено, 5 Qed, 0 аксиом. ↩

Путь Мудрости

Проводник