10. 位相

微積分は関数の概念に基づいており，互いに依存しあう量をモデル化するのに用いられます．例えば，時間とともに変化する量についての研究は一般的です．また 極限 （limit）という概念も基本的なものです．関数 \(f(x)\) の極限は \(x\) の値が \(a\) に近づくにつれて \(b\) になる，あるいは \(f(x)\) は \(x\) が \(a\) に近づくにつれて \(b\) に 収束する （converges to）と言うことができます．同様に， \(f(x)\) は \(x\) が \(a\) に近づくにつれて \(b\) に近づく，あるいは \(x\) が \(a\) に近づくにつれて \(b\) に 限りなく近づく （tends to）と言うこともできます．このような概念について Section 3.6 で既に考察しています．

位相 （Topology）は極限と連続性についての抽象的な研究です． 2 章から 6 章までで形式化の要点を説明しましたが，この章ではMathlibで位相的な概念がそのように形式化されているかを説明します．位相的な抽象化は，より一般的に適用できるだけでなく，逆説的ではありますが，具体的な事例における極限や連続性についての推論を容易にします．

位相的な概念は，数学的な構造のかなり多くのレイヤーの上に成り立っています．最初の層は素朴な集合論で， Chapter 4 で説明しています．次の層は Section 10.1 で説明する フィルタ （filter）の理論です．その上に 位相空間 （topological spaces）， 距離空間 （metric spaces），そして少し独特的な中間概念である 一様空間 （uniform space）の理論を重ねます．

これまでの章では，読者にとってなじみ深い数学的概念に頼っていましたが，フィルタの概念は現役の数学者であってもあまり知られていません．しかし，この概念は数学を効果的に形式化するためには不可欠です．その理由を説明しましょう． f : ℝ → ℝ を任意の関数とします．ここで x がある値 x₀ に近づいたときの f x の極限を考えることができますが， x が無限大や負の無限大に近づいたときの f x の極限を考えることもできます．さらに， x が右から x₀ に近づいた時（これは慣習的に x₀⁺ と書かれます），また左側から近づいたとき（ x₀⁻ と書かれます）の f x の極限を考えることもできます． x が x₀ や x₀⁺ ， x₀⁻ に近づく方法はさまざまである一方， x₀ の値自体を取ることは許可されていないとします．この結果，少なくとも8つの方法で x が何らかの値に近づくことができます． x を有理数の値に制限したり，始域にほかの制約を加えることもできますが，この8つのケースに限定することにしましょう．

また終域に同じようにいくつかのオプションを設けることができます: f x が左か右，もしくは正・負の無限などから近づくことを指定できます．例えば， x が右から x₀ にならないように限りなく x₀ に近づくとき， f x は +∞ に限りなく近づくということができます．この結果， Section 3.6 で行った数列の極限を扱い始めてないにもかかわらず，もうすでに64種類の極限に関する文が存在することになります．

極限にかかわる補題となると問題はさらに複雑になります．例えば，極限は次のように合成されます: x が x₀ に限りなく近づくときに f x が y₀ に限りなく近づき，また y が y₀ に限りなく近づくとき g y が z₀ に限りなく近づくならば， g ∘ f x は x が x₀ に限りなく近づくとき z₀ に限りなく近づきます．ここでは3つの「限りなく近づく」概念が働いており，それぞれ前の段落で説明した8つの方法のいずれかでインスタンス化することができます．この結果，512の補題が生まれ，ライブラリに追加しなければならなくなります！非形式的には，数学者は一般的にこれらのうち2つか3つを証明し，残りは「同様の方法で」証明できることを示すだけです．数学を形式化するには，この「同じ」という概念を完全に明示する必要があり，これこそブルバキのフィルタ理論が取り扱うことです．

10.1. フィルタ

型 X に対する フィルタ は，以下に述べる3つの条件を満たす X の元からなる集合のあつまりです．この概念から2つのアイデアが提供されます．

  • 極限 （limit），数列の有限・無限極限，ある点，もしくは無限大における関数の有限・無限極限など今まで議論してきたすべての極限を含んだもの

  • やがて起こりうること （things happening eventually），これは十分大きい n : ℕ ，もしくはある点 x の十分近傍について，あるいは十分近い点のペアや測度論の意味でのほぼすべての場所で起こることを含みます．また，それと対をなすようにフィルタは任意の大きさの点 n や，任意の近傍の点などについて， 頻繁に起こること （things happening often）を表現することもできます．

上記の記述に対応するフィルタはこの節の後半で定義しますが，先に名称を出しておきましょう．

  • (atTop : Filter ℕ) ，ある N について {n | n ≥ N} を含む ℕ の集合のあつまり

  • 𝓝 x ，位相空間の x の近傍のあつまり

  • 𝓤 X ，一様空間（一様空間とは距離空間と位相群を一般化したものです）の近縁のあつまり

  • μ.ae ，集合のあつまりで，各集合の補集合が測度 μ に対して零測度をもつもの

一般的な定義は以下のとおりです: フィルタ F : Filter X は以下の条件を満たす集合のあつまり F.sets : Set (Set X) です:

  • F.univ_sets : univ ∈ F.sets

  • F.sets_of_superset : ∀ {U V}, U ∈ F.sets → U ⊆ V → V ∈ F.sets

  • F.inter_sets : ∀ {U V}, U ∈ F.sets → V ∈ F.sets → U ∩ V ∈ F.sets.

最初の条件は X のすべての要素の集合は F.sets に属するというものです．2つ目の条件は U が F.sets に属する場合， U を含むものはすべて F.sets に属するということです．3つ目の条件は， F.sets は有限な共通集合で閉じているということです．Mathlibでは，フィルタ F は F.sets とその3つのプロパティをまとめた構造体として定義されていますが，プロパティはデータを追加で持つことはないため， F と F.sets の区別を曖昧にするのに便利です．したがって， U ∈ F を U ∈ F.sets の意味として定義します．これが， U ∈ F に言及する補題の名前に sets という単語が登場するものが散見される理由です．

フィルタとは，「十分大きい」集合の概念を定義するものだと考えると良いでしょう．最初の条件は univ が十分に大きいことを言い，2番めの条件は十分に大きい集合を含む集合も十分大きいことを，そして3番目の条件は十分に大きい2つの集合の共通集合が十分に大きいことを言っています．

型 X のフィルタを Set X の一般化された要素と考えるとさらに便利かもしれません．例えば， atTop は「非常に大きな数の集合」であり， 𝓝 x₀ は「 x₀ に非常に近い点の集合」です．この考え方が現れている例の1つとして，任意の s : Set X に対して s を含むすべての集合からなるいわゆる 主フィルタ （principal filter）を関連付けることができる，というものがあります．この定義はすでにMathlibに存在しており， 𝓟 という表記が与えられています．（ Filter 名前空間にローカライズされています）フィルタの定義の体験するちょうど良い機会なので，この定義に取り組んでみましょう．

def principal {α : Type*} (s : Set α) : Filter α
    where
  sets := { t | s ⊆ t }
  univ_sets := sorry
  sets_of_superset := sorry
  inter_sets := sorry

2つ目の例題として， atTop : Filter ℕ を定義してみましょう．（ ℕ の代わりに前順序を持つ任意の型を使うことができます．）

example : Filter ℕ :=
  { sets := { s | ∃ a, ∀ b, a ≤ b → b ∈ s }
    univ_sets := sorry
    sets_of_superset := sorry
    inter_sets := sorry }

また，任意の x : ℝ の近傍のフィルタ 𝓝 x を直接定義することもできます．実数において x の近傍とは開区間 \((x_0 - \varepsilon, x_0 + \varepsilon)\) を含む集合のことで，Mathlibでは Ioo (x₀ - ε) (x₀ + ε) と定義されています．（この近傍の概念は，Mathlibにおけるより一般的な構造の特殊なケースにすぎません．）

これらの例から，関数 f : X → Y がある F : Filter X に沿って G : Filter Y に収束するとはどういうことかを以下のように定義できます．

def Tendsto₁ {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) :=
  ∀ V ∈ G, f ⁻¹' V ∈ F

X が ℕ で Y が ℝ であるとき， Tendsto₁ u atTop (𝓝 x) は数列 u : ℕ → ℝ が実数 x に収束するということと等価です． X と Y の両方が ℝ であるとき， Tendsto f (𝓝 x₀) (𝓝 y₀) はおなじみの \(\lim_{x \to x₀} f(x) = y₀\) と等価です．冒頭で述べた他の種類の極限も，入力と出力のフィルタを適切に選択すれば，すべて Tendsto₁ のインスタンスと等価です．

上記の Tendsto₁ の概念はMathlibで定義されている Tendsto と定義上等価ですが，後者のほうがより抽象的に定義されています． Tendsto₁ の定義の問題点は，量化子と G の要素を公開してしまう点にあり，これによってフィルタを一般化された集合としてみなすことで得られる直感的なイメージをうすめてしまっています．量化子 ∀ V を隠し，より代数的・集合論的な仕組みを使うことで直感的なイメージをよりはっきりさせることができます．そのための最初の要素は，任意の写像 f : X → Y に関連した 押し出し （pushforward）演算子 \(f_*\) で，これはMathlibでは Filter.map f と表記されています． X 上のフィルタ F が与えられた時， Filter.map f F : Filter Y は V ∈ Filter.map f F ↔ f ⁻¹' V ∈ F が定義上成り立つように定義されています．本書のサンプルファイルでは， Filter.map を map と書けるように Filter 名前空間をオープンしています．このことは Filter Y の集合の要素の包含を逆にした順序関係を使って Tendsto の定義を書き直すことができることを意味します．つまり， G H : Filter Y が与えられると， G ≤ H ↔ ∀ V : Set Y, V ∈ H → V ∈ G が成り立ちます．

def Tendsto₂ {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) :=
  map f F ≤ G

example {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) :
    Tendsto₂ f F G ↔ Tendsto₁ f F G :=
  Iff.rfl

フィルタの順序関係が逆だと思われるかもしれません．しかし，任意の集合 s を対応する主フィルタに写す包含 𝓟 : Set X → Filter X によって， X 上のフィルタを Set X の一般化された要素としてみなすことが出来ることを思い出してください．この包含写像は順序を保存するため， Filter の順序関係は一般化された集合間の自然な包含関係とみなすことができます．この類推において，押し出しは順像に類似しています．そして実際に map f (𝓟 s) = 𝓟 (f '' s) となります．

以上から数列 u : ℕ → ℝ が点 x₀ に収束するのは map u atTop ≤ 𝓝 x₀ である場合に限る理由を直観的に理解できます．この不等式は「非常に大きな自然数の集合」の「 u の下の順像」が「 x₀ に非常に近い点の集合」に「含まれる」ことを意味します．

約束通り， Tendsto₂ の定義は量化子や集合を明示しません．また押し出し演算の代数的特性を活用しています．まず各 Filter.map f は単調です．そして第二に， Filter.map は合成と互換性があります．

#check (@Filter.map_mono : ∀ {α β} {m : α → β}, Monotone (map m))

#check
  (@Filter.map_map :
    ∀ {α β γ} {f : Filter α} {m : α → β} {m' : β → γ}, map m' (map m f) = map (m' ∘ m) f)

この2つの性質を組み合わせると，極限の合成を証明することができ，冒頭で述べた合成の256個の補題とそれ以上のものが一発で得られます．演習として上の2つの補題と一緒に普遍量化子か代数的定義による Tendsto₁ を使って以下の文を証明してみましょう．

example {X Y Z : Type*} {F : Filter X} {G : Filter Y} {H : Filter Z} {f : X → Y} {g : Y → Z}
    (hf : Tendsto₁ f F G) (hg : Tendsto₁ g G H) : Tendsto₁ (g ∘ f) F H :=
  sorry

押し出しによる構成は写像を使用して写像の入力から出力にフィルタを押し出します．また 引き戻し （pullback） Filter.comap という反対方向の演算もあります．これは集合上の逆像に対する操作を一般化したものです．任意の写像 f に対して， Filter.map f と Filter.comap f は各 F と G に対して以下を満たす ガロア接続 （Galois connection）として知られるものを形成します．

Filter.map_le_iff_le_comap : Filter.map f F ≤ G ↔ F ≤ Filter.comap f G

この操作を使ってMathlibのものと等価なことを証明できる（しかし定義的には等しくない） Tendsto の別の定式化ができます．

comap 演算はフィルタを部分型に制限するために使うことができます．例えば， f : ℝ → ℝ と x₀ : ℝ ， y₀ : ℝ があり， 有理数の範囲内で x が x₀ に近づくと f x が y₀ に近づくとします．ここで強制の写像 (↑) : ℚ → ℝ を使って 𝓝 x₀ を ℚ に引き戻すことで Tendsto (f ∘ (↑) : ℚ → ℝ) (comap (↑) (𝓝 x₀)) (𝓝 y₀) とすることができます．

variable (f : ℝ → ℝ) (x₀ y₀ : ℝ)

#check comap ((↑) : ℚ → ℝ) (𝓝 x₀)

#check Tendsto (f ∘ (↑)) (comap ((↑) : ℚ → ℝ) (𝓝 x₀)) (𝓝 y₀)

引き戻し演算も合成と互換性がありますが，こちらは 反変 （contravariant），つまり引数の順序を逆にします．

section
variable {α β γ : Type*} (F : Filter α) {m : γ → β} {n : β → α}

#check (comap_comap : comap m (comap n F) = comap (n ∘ m) F)

end

ここで平面 ℝ × ℝ に目を向けて，点 (x₀, y₀) の近傍が 𝓝 x₀ と 𝓝 y₀ にどのように関係しているか考えてみましょう．この問いの答えは ×ˢ と表記される積の演算 Filter.prod : Filter X → Filter Y → Filter (X × Y) です:

example : 𝓝 (x₀, y₀) = 𝓝 x₀ ×ˢ 𝓝 y₀ :=
  nhds_prod_eq

積演算は引き戻し演算と inf 演算で定義されています．

F ×ˢ G = (comap Prod.fst F) ⊓ (comap Prod.snd G).

ここで inf 演算は任意の型 X に対する Filter X 上の束構造を指し， F ⊓ G は F と G の両方よりも小さい最大のフィルターです．このように， inf 演算は集合の共通部分の概念を一般化したものです．

Mathlibの多くの証明では，前述の構造（ map ， comap ， inf ， sup ， prod ）をすべて使用して，フィルタのメンバを参照することなく収束に関する代数的な証明を行っています．このスタイルの練習として，以下の補題を Tendsto と Filter.prod の定義を展開しながら証明してみましょう．

#check le_inf_iff

example (f : ℕ → ℝ × ℝ) (x₀ y₀ : ℝ) :
    Tendsto f atTop (𝓝 (x₀, y₀)) ↔
      Tendsto (Prod.fst ∘ f) atTop (𝓝 x₀) ∧ Tendsto (Prod.snd ∘ f) atTop (𝓝 y₀) :=
  sorry

順序型として Filter X は実際に 完備 （complete）な束です．つまり，ボトムの要素とトップの要素があり， X 上のフィルタのすべての集合は Inf と Sup を持ちます．

フィルタの定義中の2つ目の性質（ U が F に属するのであれば， U より大きいものすべてが F に属する）を考えると，1つ目の性質（ X のすべての要素からなる集合は F に属する）は F が集合の集まりとして空ではないという性質と等価であることに注意してください．これは空集合が F の 要素 であるかどうかという，より微妙な問題と混同してはいけません．フィルタの定義は ∅ ∈ F を禁止していませんが，もし空集合が F に含まれるなら，すべての集合は F に含まれることに成ります．この場合， F は完備束 Filter X のボトムの要素であるとても自明なものになります．これはブルバキにおける空集合を含むフィルタは許さないとしてフィルタの定義とは対照的です．

本書の定義には自明なフィルタが含まれているため，いくつかの補題では非自明性を明示的に仮定する必要があります．しかし，その代わりに理論はより良い大域的な性質を持ちます．自明なフィルタを含めるとボトムの要素が得られることは既に見ました．また空集合を除外する前提条件なしに， ∅ を ⊥ に写す principal : Set X → Filter X を定義することもできます．さらに引き戻し演算も同様に前提条件なしで定義できます．実際， F ≠ ⊥ であるにもかかわらず， comap f F = ⊥ が成り立つことがあります．例えば， x₀ : ℝ と s : Set ℝ が与えられた時， x₀ が s の閉包に属する場合に限り， s に対応する部分型からの強制下での 𝓝 x₀ の引き戻しは自明ではありません．

自明でないフィルタがあることを仮定する補題を管理するために，Mathlibには Filter.NeBot という型クラスがあり，ライブラリ中の補題では (F : Filter X) [F.NeBot] というように利用しています．インスタンスのデータベースは，例えば (atTop : Filter ℕ).NeBot があること，また自明でないフィルタを押し出すと自明でないフィルタが得られることを知っています．その結果， [F.NeBot] を仮定した補題は任意の数列 u の map u atTop に対して自動的に適用されます．

フィルタの代数的な性質と極限との関係についての基本的な紹介は終了しましたが，通常の極限の概念を再現したという主張を正当化するには至っていません．表面的には Tendsto u atTop (𝓝 x₀) は Section 3.6 で定義されている収束の概念よりも強いです．なぜなら，上記の定義では x₀ の すべて の近傍に atTop に属する逆像があることを求めているのに対し，通常の定義では，標準的な近傍 Ioo (x₀ - ε) (x₀ + ε) に対してのみ求めているからです．重要なのは，定義上すべての近傍はこのような標準的な近傍をすべて含むということです．この観察は フィルタ基底 （filter basis）という概念に繋がります．

F : Filter X が与えられた時，集合の族 s : ι → Set X が F の基底であるとは，すべての集合 U に対して，ある s i を含む場合に限り U ∈ F が成り立つことを言います．形式的に言い換えると， s は ∀ U : Set X, U ∈ F ↔ ∃ i, s i ⊆ U を満たす場合に基底となります．添字型の値 i の一部のみを取るような ι に対する述語として考えるとさらに柔軟です．例えば 𝓝 x₀ の場合， ι を ℝ ， i を ε とし， ε が正の値を取るという述語になります．そこで，集合 Ioo  (x₀ - ε) (x₀ + ε) が ℝ 上の近傍位相の基底を形成するという事実は以下のように述べられます．

example (x₀ : ℝ) : HasBasis (𝓝 x₀) (fun ε : ℝ ↦ 0 < ε) fun ε ↦ Ioo (x₀ - ε) (x₀ + ε) :=
  nhds_basis_Ioo_pos x₀

またフィルタ atTop に対する良い基底もあります．補題 Filter.HasBasis.tendsto_iff を使えば， F と G の基底が与えられたときに， Tendsto f F G という形の文を再形式化することができます．これらをまとめると， Section 3.6 で取り扱った収束の本質的な概念が得られます．

example (u : ℕ → ℝ) (x₀ : ℝ) :
    Tendsto u atTop (𝓝 x₀) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ∈ Ioo (x₀ - ε) (x₀ + ε) := by
  have : atTop.HasBasis (fun _ : ℕ ↦ True) Ici := atTop_basis
  rw [this.tendsto_iff (nhds_basis_Ioo_pos x₀)]
  simp

ここからは，十分に大きな数や与えられた点に十分近い点に対して成り立つ性質をフィルタによって容易に扱える方法を示します． Section 3.6 では，ある性質 P n が十分に大きい n に対して成り立ち，他の性質 Q n が十分に大きい n に対して成り立つという状況によく直面しました．この場合 cases を2回使うと， ∀ n ≥ N_P, P n と ∀ n ≥ N_Q, Q n を満たす N_P と N_Q が得られます．そして set N := max N_P N_Q を使うことでようやく ∀ n ≥ N, P n ∧ Q n を証明することができます．これを繰り返すのは面倒です．

「 P n と Q n は十分な大きさの n に対して成り立つ」という文が {n | P n} ∈ atTop と {n | Q n} ∈ atTop が成り立つことを意味する点に注意すればうまくいきます． atTop がフィルタであるということは， atTop の2つの要素の共通部分もまた atTop の中にあることを意味するので， {n | P n ∧ Q n} ∈ atTop となります． {n | P n} ∈ atTop と書くのは好ましくないため，より示唆的な表記として ∀ᶠ n in atTop, P n を使うことができます．ここで上付き文字の f は Filter を表しています．この表記は「非常に大きな数の集合」に含まれるすべての n に対して P n が成り立つということだと考えることができます． ∀ᶠ という表記は Filter.Eventually を意味し，また補題 Filter.Eventually.and は先程説明したフィルタの共通部分の性質を使っています:

example (P Q : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n) :
    ∀ᶠ n in atTop, P n ∧ Q n :=
  hP.and hQ

この表記法は非常に便利で直感的であるため， P が等式または不等式である場合の特殊版も存在します．例えば， u と v を2つの実数の列とします．そして u n と v n が十分に大きい n で一致する場合， v が x₀ に収束する場合に限り u が x₀ に収束することを示しましょう．以下の1つ目では一般的な Eventually を使い，次の例では等式の述語に特化した EventuallyEq を用います．この2つの文は定義上等しいため，どちらの場合でも同じ証明が通ります．

example (u v : ℕ → ℝ) (h : ∀ᶠ n in atTop, u n = v n) (x₀ : ℝ) :
    Tendsto u atTop (𝓝 x₀) ↔ Tendsto v atTop (𝓝 x₀) :=
  tendsto_congr' h

example (u v : ℕ → ℝ) (h : u =ᶠ[atTop] v) (x₀ : ℝ) :
    Tendsto u atTop (𝓝 x₀) ↔ Tendsto v atTop (𝓝 x₀) :=
  tendsto_congr' h

フィルタの定義を Eventually の観点から復習することは有益です． X 上の任意の述語 P と Q に対して F : Filter X が与えられたとしたとき，

  • 条件 univ ∈ F は (∀ x, P x) → ∀ᶠ x in F, P x を，

  • 条件 U ∈ F → U ⊆ V → V ∈ F は (∀ᶠ x in F, P x) → (∀ x, P x → Q x) → ∀ᶠ x in F, Q x を，

  • 条件 U ∈ F → V ∈ F → U ∩ V ∈ F は (∀ᶠ x in F, P x) → (∀ᶠ x in F, Q x) → ∀ᶠ x in F, P x ∧ Q x を保証します．

#check Eventually.of_forall
#check Eventually.mono
#check Eventually.and

2つ目の項目は Eventually.mono に対応し，特に Eventually.and と組み合わせることでフィルタの良い扱い方をサポートします． filter_upwards タクティクはこの組み合わせを行ってくれます．比較してみましょう：

example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n)
    (hR : ∀ᶠ n in atTop, P n ∧ Q n → R n) : ∀ᶠ n in atTop, R n := by
  apply (hP.and (hQ.and hR)).mono
  rintro n ⟨h, h', h''⟩
  exact h'' ⟨h, h'⟩

example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n)
    (hR : ∀ᶠ n in atTop, P n ∧ Q n → R n) : ∀ᶠ n in atTop, R n := by
  filter_upwards [hP, hQ, hR] with n h h' h''
  exact h'' ⟨h, h'⟩

測度論を知っている読者なら，補集合が測度0である集合のフィルタ μ.ae （いわゆる「ほとんどすべての点からなる集合」）は Tendsto の入力や出力としてはあまり役に立たないことに気づくでしょう．しかし， Eventually と一緒に使ってほとんどすべての点で成り立つ性質について言及する場合には便利です．

∀ᶠ x in F, P x には {x | ¬P x} ∉ F を意味する双対バージョン ∃ᶠ x in F, P x があり，これは時折役立ちます．例えば， ∃ᶠ n in atTop, P n は P n が成り立つような任意の大きさの n が存在することを意味します． ∃ᶠ は Filter.Frequently を表します．

より複雑な例として，数列 u ，集合 M ，値 x についての以下の文を考えてみましょう．

もし u が x に収束し，十分大きい n について u n が M に属するならば， x は M の閉包の中にある．

これは以下のように形式化されます：

Tendsto u atTop (𝓝 x) → (∀ᶠ n in atTop, u n ∈ M) → x ∈ closure M.

これは位相についてのライブラリの定理 mem_closure_of_tendsto の特殊な場合です．以下に掲げた補題と ClusterPt x F が (𝓝 x ⊓ F).NeBot を，仮定 ∀ᶠ n in atTop, u n ∈ M が定義上 M ∈ map u atTop を意味するという事実を用いて証明してみましょう．

#check mem_closure_iff_clusterPt
#check le_principal_iff
#check neBot_of_le

example (u : ℕ → ℝ) (M : Set ℝ) (x : ℝ) (hux : Tendsto u atTop (𝓝 x))
    (huM : ∀ᶠ n in atTop, u n ∈ M) : x ∈ closure M :=
  sorry

10.2. 距離空間

前節の例題は実数の数列に焦点をあてました．このセクションでは一般性を少し上げて距離空間(metric space)に焦点をあてます．距離空間とは距離関数 dist : X → X → ℝ を持つ X 型のことで， fun x y ↦ |x - y| を X = ℝ の場合から一般化したものです．

このような空間の導入は簡単で，距離関数から必要な特性をすべて確認できます．

variable {X : Type*} [MetricSpace X] (a b c : X)

#check (dist a b : ℝ)
#check (dist_nonneg : 0 ≤ dist a b)
#check (dist_eq_zero : dist a b = 0 ↔ a = b)
#check (dist_comm a b : dist a b = dist b a)
#check (dist_triangle a b c : dist a c ≤ dist a b + dist b c)

また，距離が無限大になるものや， a = b でなくとも dist a b が0になるもの，あるいはその両方が存在するものもあります．これらはそれぞれ EMetricSpace ， PseudoMetricSpace ， PseudoEMetricSpace と呼ばれます（ここで”e”は”extends”を表します）． ℝ から距離空間への旅は線形代数を必要とするノルム空間の特殊なケースを飛び越えたことに注意してください．ノルム空間については微積分の章で説明します．

10.2.1. 収束と連続性

距離関数を使えば，収束列と距離空間のあいだの連続関数を定義できます．これらの関数は実際には次節で説明する，より一般的な設定で定義されています．しかし，この定義を距離の用語に置き換えた補題があります．

example {u : ℕ → X} {a : X} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε :=
  Metric.tendsto_atTop

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} :
    Continuous f ↔
      ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε :=
  Metric.continuous_iff

多く の補題が連続性を仮定しているため，たくさんの連続性の結果を証明するはめになります．このタスクのために continuity タクティクが用意されています．以下の演習問題で必要と成る連続性を証明してみましょう．Leanは2つの距離空間の積を距離空間として扱う方法を知っているため， X × X から ℝ への連続関数を考えることは理にかなっています．特に（非カリー化された）距離関数がそのような関数です．

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := by continuity

このタクティクは少し挙動が遅いため，これと同等の内容を手作業で行う方法を知っておくと良いでしょう．まず fun p : X × X ↦ f p.1 が連続であるという事実を使う必要があります．この事実は仮定 hf によって連続である f と補題 continuous_fst の内容から連続性を持つ prod.fst との合成から成り立ちます．この合成の性質は Continuous.comp によるものです．これは Continuous 名前空間にあるため， Continuous.comp hf continuous_fst という書き方はドットによる表記法で hf.comp continuous_fst に短縮することができます．こうすることでまさに仮定と補題を合成しているというように読めるため，より可読性が上がります．2つ目の構成要素についても同じようにして fun p : X × X ↦ f p.2 の連続性が得られます．次にこの2つの連続性を Continuous.prod_mk を使って (hf.comp continuous_fst).prod_mk (hf.comp continuous_snd) : Continuous (fun p : X × X ↦ (f p.1, f p.2)) となり，またもう一回合成することで完全な証明になります．

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  continuous_dist.comp ((hf.comp continuous_fst).prod_mk (hf.comp continuous_snd))

Continuous.prod_mk と Continuous.comp を介した continuous_dist の組み合わせは，仮に上記のようなドット表記を多用したとしても不格好になってしまいます．しかしより重要な問題はこの綺麗な証明を構築するには事前に多くの計画をする必要があるということです．Leanが上記の証明項を受け入れるのは，それがゴールと定義的に等価な文を証明する完全な項だからです．実際，ゴールの関数 fun p : X × X ↦ dist (f p.1) (f p.2) は合成として提示されていません．上記の証明項は dist ∘ (fun p : X × X ↦ (f p.1, f p.2)) の連続性を目標の関数とたまたま定義的に等しいことから証明しています．しかし，この証明を apply continuous_dist.comp から始まるタクティクスタイルで逐次的に構築しようとすると，Leanのエラボレータは合成を認識できず，この補題の適用を拒否します．特に型の積が関係する場合を苦手としています．

ここではむしろ補題 Continuous.dist {f g : X → Y} : Continuous f → Continuous g → Continuous (fun x ↦ dist (f x) (g x)) を適用するのがよいでしょう．これはLeanのエラボレータにとってより良いものであり，また先程の文に対する以下の2つの新しい証明からわかるように，完全な証明項がより短くなります：

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := by
  apply Continuous.dist
  exact hf.comp continuous_fst
  exact hf.comp continuous_snd

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  (hf.comp continuous_fst).dist (hf.comp continuous_snd)

合成から生じるエラボレータの問題を除けば，証明を圧縮する別の方法は Continuous.prod_map を使うことです．これは時に便利で，これによってより短い証明項 continuous_dist.comp (hf.prod_map hf) を与えます．

エラボレータに都合の良いバージョンと型に対して短くなるバージョンの間を決めるのはツライため，この議論は Continuous.fst' が提供する圧縮の最後のひと手間を加えることで， hf.comp continuous_fst を hf.fst' に（ snd も同様）圧縮することができ，難読化との境界を超えた最終的な証明を得ることができます．

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  hf.fst'.dist hf.snd'

今度は読者が連続性の補題を証明する番です．continuityタクティクを使った後に，手作業で Continuous.add ， continuous_pow ， continuous_id を使う必要があります．

example {f : ℝ → X} (hf : Continuous f) : Continuous fun x : ℝ ↦ f (x ^ 2 + x) :=
  sorry

ここまではグローバルな概念としての連続性を見てきましたが，ある点での連続性を定義することもできます．

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) (a : X) :
    ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x}, dist x a < δ → dist (f x) (f a) < ε :=
  Metric.continuousAt_iff

10.2.2. 球体，開集合，閉集合

距離関数を得たので，次は最も重要な幾何学的定義である（開）球体と閉球体です．

variable (r : ℝ)

example : Metric.ball a r = { b | dist b a < r } :=
  rfl

example : Metric.closedBall a r = { b | dist b a ≤ r } :=
  rfl

ここで r は任意の実数であり，符号の制限が無いことに注目してください．もちろん，半径の条件が必要な文も存在します．

example (hr : 0 < r) : a ∈ Metric.ball a r :=
  Metric.mem_ball_self hr

example (hr : 0 ≤ r) : a ∈ Metric.closedBall a r :=
  Metric.mem_closedBall_self hr

球体があれば，開集合を定義することができます．実際には，開集合は次の節で説明するより一般的な設定で定義されますが，ここでは球体による定義に変更した補題を使います．

example (s : Set X) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s :=
  Metric.isOpen_iff

また閉集合とは，補集合が開である集合のことです．この集合についての重要な性質は，極限のもとで閉じていることです．ある集合の閉包は，その集合を含む最小の閉集合です．

example {s : Set X} : IsClosed s ↔ IsOpen (sᶜ) :=
  isOpen_compl_iff.symm

example {s : Set X} (hs : IsClosed s) {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a))
    (hus : ∀ n, u n ∈ s) : a ∈ s :=
  hs.mem_of_tendsto hu (Eventually.of_forall hus)

example {s : Set X} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, a ∈ Metric.ball b ε :=
  Metric.mem_closure_iff

次の演習問題を mem_closure_iff_seq_limit を使わずに証明してみましょう．

example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) :
    a ∈ closure s :=
  sorry

フィルタについての節で，Mathlibでは近傍のフィルタが大きな役割を果たしていたことを思い出してください．距離空間の文脈での重要なポイントは，球体がこれらのフィルタの基底となることです．ここでの主な補題は Metric.nhds_basis_ball と Metric.nhds_basis_closedBall で，正の半径を持つ開球と閉球に対して主張されるものです．中心点は暗黙の引数であるため，次の例のように Filter.HasBasis.mem_iff を呼び出すことができます．

example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s :=
  Metric.nhds_basis_ball.mem_iff

example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.closedBall x ε ⊆ s :=
  Metric.nhds_basis_closedBall.mem_iff

10.2.3. コンパクト性

コンパクト性は位相幾何学的に重要な概念です．これは他の区間と比べて実数の線分に近い性質を満足する距離空間の部分集合を識別するものです：

  • コンパクトな集合から値を取る数列はこの集合内に収束する部分列を持つ

  • 実数値を持つ空でないコンパクトな集合上の連続関数はすべて境界を持ち，どこかでその境界に到達する（これを極値の定理と呼びます）

  • コンパクトな集合は閉集合である

まず，実数の単位区間が実際にコンパクト集合であることを確認し，次に一般的な距離空間のコンパクト集合について上記の主張を確認してみましょう．2つ目の文では，与えられた集合の連続性だけが必要であるため， Continuous の代わりに ContinuousOn を使い，最小値と最大値について別々の命題を与えます．もちろん，これらの結果はすべてより一般的なものから導かれます．そのうちのいくつかはこの後の節で議論します．

example : IsCompact (Set.Icc 0 1 : Set ℝ) :=
  isCompact_Icc

example {s : Set X} (hs : IsCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) :
    ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) :=
  hs.tendsto_subseq hu

example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ}
      (hfs : ContinuousOn f s) :
    ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y :=
  hs.exists_isMinOn hs' hfs

example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ}
      (hfs : ContinuousOn f s) :
    ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x :=
  hs.exists_isMaxOn hs' hfs

example {s : Set X} (hs : IsCompact s) : IsClosed s :=
  hs.isClosed

また， Prop-値の型クラスを追加することで，距離空間が大域的にコンパクトであることを指定することもできます：

example {X : Type*} [MetricSpace X] [CompactSpace X] : IsCompact (univ : Set X) :=
  isCompact_univ

コンパクトな距離空間において，すべての閉集合はコンパクトです．これが IsClosed.isCompact です．

10.2.4. 一様連続関数

ここで距離空間の一様性に立ち入りましょう：例えば一様連続関数，コーシー列，完全性などです．これらもまたより一般的な文脈で定義されますが，それらの初歩的な定義に触れるために距離の名前空間での補題を作りましょう．まず一様連続性から始めましょう．

example {X : Type*} [MetricSpace X] {Y : Type*} [MetricSpace Y] {f : X → Y} :
    UniformContinuous f ↔
      ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε :=
  Metric.uniformContinuous_iff

これらの定義をすべて扱う練習として，コンパクトな距離空間から距離空間への連続関数が一様に連続であることを証明します．（後の節でより一般的なバージョンを見ます）

まず非形式的な証明のあらすじを説明しましょう． f : X → Y をコンパクトな距離空間から距離空間への連続関数とします．ここで， ε > 0 を固定し，ある δ を探し始めます．

φ : X × X → ℝ := fun p ↦ dist (f p.1) (f p.2) と K := { p : X × X | ε ≤ φ p } を仮定します． f と距離は連続であるため， φ は連続です．また， K は明らかに閉じている（ isClosed_le を使います）ので， X はコンパクトであることから K はコンパクトになります．

ここで eq_empty_or_nonempty を使って2つの可能性を議論します．もし， K が空であれば，明らかに成り立ちます（例えば δ = 1 と設定できます）．そこで， K が空でないと仮定し，極値の定理を使って (x₀, x₁) を選択し， K 上の距離関数の下限を求めます．そして δ = dist x₀ x₁ と設定し，これがうまくいくことを確認します．

example {X : Type*} [MetricSpace X] [CompactSpace X]
      {Y : Type*} [MetricSpace Y] {f : X → Y}
    (hf : Continuous f) : UniformContinuous f :=
  sorry

10.2.5. 完全性

距離空間におけるコーシー列とは，各項がどんどん互いに近づいていく数列のことです．この考え方にはいくつかの等価な言い方があります．特に収束する数列はコーシー列です．その逆はいわゆる 完全 （complete）空間においてのみ成り立ちます．

example (u : ℕ → X) :
    CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε :=
  Metric.cauchySeq_iff

example (u : ℕ → X) :
    CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε :=
  Metric.cauchySeq_iff'

example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) :
    ∃ x, Tendsto u atTop (𝓝 x) :=
  cauchySeq_tendsto_of_complete hu

この定義を使う練習として以下の便利な条件を証明しましょう．これはMathlibに登場する条件の特殊なケースです．また，これは幾何学的な文脈で大きな和を使う練習をする良い機会でもあります．フィルタのセクションの説明に加えて，おそらく tendsto_pow_atTop_nhds_zero_of_lt_one と Tendsto.mul ， dist_le_range_sum_dist が必要になるでしょう．

theorem cauchySeq_of_le_geometric_two' {u : ℕ → X}
    (hu : ∀ n : ℕ, dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n) : CauchySeq u := by
  rw [Metric.cauchySeq_iff']
  intro ε ε_pos
  obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε := by sorry
  use N
  intro n hn
  obtain ⟨k, rfl : n = N + k⟩ := le_iff_exists_add.mp hn
  calc
    dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry
    _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
    _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry
    _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := sorry
    _ ≤ 1 / 2 ^ N * 2 := sorry
    _ < ε := sorry

本節のラスボスへ挑む準備が整いました：完全距離空間に対するベールの定理です！以下の証明の骨組みでは興味深いテクニックを駆使しています．これは choose タクティクを使っており（このビックリマークを削除してみることをおすすめします）， Nat.rec_on を使って証明の途中で帰納的に何かを定義する方法を示しています．

open Metric

example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : ∀ n, Dense (f n)) :
    Dense (⋂ n, f n) := by
  let B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
  have Bpos : ∀ n, 0 < B n
  sorry
  /- Translate the density assumption into two functions `center` and `radius` associating
    to any n, x, δ, δpos a center and a positive radius such that
    `closedBall center radius` is included both in `f n` and in `closedBall x δ`.
    We can also require `radius ≤ (1/2)^(n+1)`, to ensure we get a Cauchy sequence later. -/
  have :
    ∀ (n : ℕ) (x : X),
      ∀ δ > 0, ∃ y : X, ∃ r > 0, r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n :=
    by sorry
  choose! center radius Hpos HB Hball using this
  intro x
  rw [mem_closure_iff_nhds_basis nhds_basis_closedBall]
  intro ε εpos
  /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x`
    belonging to all `f n`. For this, we construct inductively a sequence
    `F n = (c n, r n)` such that the closed ball `closedBall (c n) (r n)` is included
    in the previous ball and in `f n`, and such that `r n` is small enough to ensure
    that `c n` is a Cauchy sequence. Then `c n` converges to a limit which belongs
    to all the `f n`. -/
  let F : ℕ → X × ℝ := fun n ↦
    Nat.recOn n (Prod.mk x (min ε (B 0)))
      fun n p ↦ Prod.mk (center n p.1 p.2) (radius n p.1 p.2)
  let c : ℕ → X := fun n ↦ (F n).1
  let r : ℕ → ℝ := fun n ↦ (F n).2
  have rpos : ∀ n, 0 < r n := by sorry
  have rB : ∀ n, r n ≤ B n := by sorry
  have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n := by
    sorry
  have cdist : ∀ n, dist (c n) (c (n + 1)) ≤ B n := by sorry
  have : CauchySeq c := cauchySeq_of_le_geometric_two' cdist
  -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.
  rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩
  -- this point `y` will be the desired point. We will check that it belongs to all
  -- `f n` and to `ball x ε`.
  use y
  have I : ∀ n, ∀ m ≥ n, closedBall (c m) (r m) ⊆ closedBall (c n) (r n) := by sorry
  have yball : ∀ n, y ∈ closedBall (c n) (r n) := by sorry
  sorry

10.3. 位相空間

10.3.1. 基礎

ここでは一般性を高めて，位相空間を紹介しましょう．まず位相空間を定義する主な方法のうち2つを復習し，位相空間の圏が距離空間の圏よりもずっと良い振る舞いをしていることを説明します．ここでは，Mathlibの圏論ライブラリを使うのではなく，圏論的な視点を持つだけにとどまることに注意してください．

距離空間から位相空間への移行を考え方の1つ目は，開集合の概念（あるいはそれに準ずる閉集合の概念）だけを覚えておくことです．この観点から，位相空間は開集合と呼ばれる集合の集まりを備えた型です．この集合は，以下に示すいくつかの公理を満たす必要があります（これらは若干冗長ですが，置いておくこととします）．

section
variable {X : Type*} [TopologicalSpace X]

example : IsOpen (univ : Set X) :=
  isOpen_univ

example : IsOpen (∅ : Set X) :=
  isOpen_empty

example {ι : Type*} {s : ι → Set X} (hs : ∀ i, IsOpen (s i)) : IsOpen (⋃ i, s i) :=
  isOpen_iUnion hs

example {ι : Type*} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen (s i)) :
    IsOpen (⋂ i, s i) :=
  isOpen_iInter_of_finite hs

また，閉集合はその補集合が開である集合として定義されます．位相空間の間の関数は開集合の逆像がすべて開であれば（大域的に）連続です．

variable {Y : Type*} [TopologicalSpace Y]

example {f : X → Y} : Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) :=
  continuous_def

この定義から，距離空間と比較して位相空間は連続関数について議論するのに十分な情報しか保有していないことがわかるでしょう．つまり，ある型上の2つの位相構造が同じであるのは，それらが同じ連続関数を持つ場合に限ります（実際，恒等関数は2つの構造が同じ開集合を持つ場合に限り両方向に連続です）．

しかし，ある点での連続性について考えると，すぐに開集合に基づくアプローチの限界が見えてきます．Mathlibでは，位相空間を，各点 x に対応する近傍フィルタ 𝓝 x を備えた型として考えることが多いです（対応する関数 X → Filter X はこの後で説明するある条件を満たします）．フィルタのセクションで，これらの道具が2つの関連した役割を果たしていたことを思い出してください．まず， 𝓝 x は x に近い X の点の一般化された集合だとみなされます．また，任意の述語 P : X → Prop に対して，この述語が x に十分近い点に対して成り立つことを示す方法を与えるものともみなされます．これらを用いて f : X → Y が x で連続であることを定義しましょう．純粋にフィルタ的な言い方をすれば， x に近い点からなる一般化された集合に対する f の順像が， f x に近い点からなる一般化された集合に含まれるということです．これは map f (𝓝 x) ≤ 𝓝 (f x) ，または Tendsto f (𝓝 x) (𝓝 (f x)) と表記されたことを思い出してください．

example {f : X → Y} {x : X} : ContinuousAt f x ↔ map f (𝓝 x) ≤ 𝓝 (f x) :=
  Iff.rfl

また近傍を通常の集合として，近傍フィルタを一般化された集合としてみなすことの両方を用いて，次のように記述することもできます．「 f x の任意の近傍 U に対して， x に近い点はすべて U に送られる」．この証明も iff.rfl で与えられ，この観点は前のものと定義上等価であることに注意してください．

example {f : X → Y} {x : X} : ContinuousAt f x ↔ ∀ U ∈ 𝓝 (f x), ∀ᶠ x in 𝓝 x, f x ∈ U :=
  Iff.rfl

ここで上記の2つの観点について，一方の視点から他方の視点に移る方法を説明しましょう．開集合の観点からは，単純に x を含む開集合を含む集合を 𝓝 x の要素と定義することができます．

example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t :=
  mem_nhds_iff

上記の反対方向へ行くにあたって，位相の近傍関数であるためには， 𝓝 : X → Filter X が満たすべき条件について議論する必要があります．

最初の制約は，一般化された集合としてみた 𝓝 x は，集合 {x} を一般化された集合としてみた pure x を含むということです（この奇妙な名前を説明すると余談が多くなるため，今はただそういうものなんだと思ってください）．別の言い方をすれば，ある述語 x に近い点で成り立つなら，それは x で成り立つということです．

example (x : X) : pure x ≤ 𝓝 x :=
  pure_le_nhds x

example (x : X) (P : X → Prop) (h : ∀ᶠ y in 𝓝 x, P y) : P x :=
  h.self_of_nhds

そして，より微妙な要件は，任意の述語 P : X → Prop と任意の x について， x に近い y に対して P y が成り立つなら， x に近い y と y に近い z に対して P z が成り立つということです．より正確には次のように成ります：

example {P : X → Prop} {x : X} (h : ∀ᶠ y in 𝓝 x, P y) : ∀ᶠ y in 𝓝 x, ∀ᶠ z in 𝓝 y, P z :=
  eventually_eventually_nhds.mpr h

この2つの結果から X → Filter X の型をもつ関数が X 上の位相空間構造の近傍関数であることが特徴づけられます．これ以外に TopologicalSpace.mkOfNhds : (X → Filter X) → TopologicalSpace X という関数も存在しますが，これは上記の2つの制約を満たす場合にのみ入力を近傍関数として返します．より正確にはこのことを別の方法で述べている TopologicalSpace.nhds_mkOfNhds があり，次の演習ではこの方法を導きます．

example {α : Type*} (n : α → Filter α) (H₀ : ∀ a, pure a ≤ n a)
    (H : ∀ a : α, ∀ p : α → Prop, (∀ᶠ x in n a, p x) → ∀ᶠ y in n a, ∀ᶠ x in n y, p x) :
    ∀ a, ∀ s ∈ n a, ∃ t ∈ n a, t ⊆ s ∧ ∀ a' ∈ t, s ∈ n a' :=
  sorry

TopologicalSpace.mkOfNhds はそれほど頻繁に使われるものではありませんが，位相空間の構造において近傍フィルタの正確な意味での定義を知っておくことは良いことでしょう．

Mathlibで位相空間を効率的に使うために知っておくべきことの2番目は， TopologicalSpace : Type u → Type u の形式的性質をたくさん使うということです．純粋数学の観点から見ると，これらの形式的特性は位相空間による距離空間が持つ問題の解決策を説明する非常に綺麗な方法です．この観点からすると，距離空間が関手性ほとんど満たしておらず，一般に圏としての性質が非常に悪いという問題が位相空間によって解決されます．このことは，既に述べたように距離空間には位相には関係ない幾何学的な情報がたくさん含まれている事実の上に成り立っています．

まず関手性に着目しましょう．距離空間の構造は部分集合に誘導することができ，また同様に単射な写像によって引き戻すこともできます．しかし，これらの条件がほぼ全てになります．一般的な写像によって引き戻されることはなく，またたとえ全射な写像であっても押し出されることもありません．

特に，距離空間の商や，距離空間の不可算積上の実用的な距離は存在しません．例えば ℝ → ℝ という型を考えてみましょう．これは ℝ をインデックスとする ℝ のコピーの積として見ることができます．関数列の点ごとの収束は，立派に収束の概念であると言いたいところです．しかし， ℝ → ℝ 上にはこの収束の概念を与える距離は存在しません．これに関連して，写像 f : X → (ℝ → ℝ) がすべての t : ℝ に対して fun x ↦ f x t が連続である場合に限り連続であることを保証する距離は存在しません．

ここでこれらの問題を解決するための情報を見直しましょう．まず，任意の写像 f : X → Y をつかって位相を一方から他方へ押し出したり引き戻したりすることができます．この2つの操作はガロア接続を形成します．

variable {X Y : Type*}

example (f : X → Y) : TopologicalSpace X → TopologicalSpace Y :=
  TopologicalSpace.coinduced f

example (f : X → Y) : TopologicalSpace Y → TopologicalSpace X :=
  TopologicalSpace.induced f

example (f : X → Y) (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) :
    TopologicalSpace.coinduced f T_X ≤ T_Y ↔ T_X ≤ TopologicalSpace.induced f T_Y :=
  coinduced_le_iff_le_induced

これらの操作は関数の合成でコンパクトにできます．例によって押し出しは共変であり，引き戻しは反変です（ coinduced_compose と induced_compose を参照）．本書では， TopologicalSpace.coinduced f T に対して \(f_*T\) ， TopologicalSpace.induced f T に対して \(f^*T\) という表記を使用します． 次の大きなピースは，任意の構造に対する TopologicalSpace X 上の完備束構造です．位相が主に開集合のあつまりであると考えるなら， TopologicalSpace X 上の順序関係は Set (Set X) から導かれると予想されます．つまり，集合 u が t' に対して開であれば， t に対して開である時に t ≤ t' になると予想するでしょう．しかし，Mathlibは開集合よりも近傍に重点を置いているので，任意の x : X に対して，位相空間から近傍への写像 fun T : TopologicalSpace X ↦ @nhds X T x は順序を保存してほしいです．そして， Filter X の順序関係は principal : Set X → Filter X が順序を保存するように設計されており，またフィルタを一般化した集合と見ることができることは既に見ました．つまり， TopologicalSpace X の順序関係は Set (Set X) の順序関係とは逆向きになります．

example {T T' : TopologicalSpace X} : T ≤ T' ↔ ∀ s, T'.IsOpen s → T.IsOpen s :=
  Iff.rfl

ここで押し出し（もしくは引き戻し）操作と順序関係を組み合わせることで，連続性を再度示すことができます．

example (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) (f : X → Y) :
    Continuous f ↔ TopologicalSpace.coinduced f T_X ≤ T_Y :=
  continuous_iff_coinduced_le

この定義と，押し出しと合成の互換性によって，任意の位相空間 \(Z\) に対して，関数 \(g : Y → Z\) が \(f_*T_X\) において連続であるのは \(g ∘ f\) が連続である場合に限るという普遍的な性質をただで手に入れることができます．

\[\begin{split}g \text{ continuous } &⇔ g_*(f_*T_X) ≤ T_Z \\ &⇔ (g ∘ f)_* T_X ≤ T_Z \\ &⇔ g ∘ f \text{ continuous}\end{split}\]
example {Z : Type*} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z)
      (g : Y → Z) :
    @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔
      @Continuous X Z T_X T_Z (g ∘ f) := by
  rw [continuous_iff_coinduced_le, coinduced_compose, continuous_iff_coinduced_le]

つまり，すでに（射影写像として f を使うことで）商位相を得ているのです．これは TopologicalSpace X がすべての X に対して完備束であるという事実を利用したものではありません．ではこのような構造によって抽象的な無意味から積位相の存在がどのように証明されるか見てみましょう．上では ℝ → ℝ の場合だけを考えましたが，ここでは ι : Type* と X : ι → Type* に対する Π i, X i の一般的な場合を考えてみましょう．任意の位相空間 Z と任意の関数 f : Z → Π i, X i に対して， f が連続であるのは，すべての ι に対して (fun x ↦ x i) ∘ f が連続である場合に限ってほしいです．ここでは射影 (fun (x : Π i, X i) ↦ x i) の表記 \(p_i\) を用いて，その制約を「紙の上で」調べてみましょう：

したがって， Π i, X i の位相が求まります．

example (ι : Type*) (X : ι → Type*) (T_X : ∀ i, TopologicalSpace (X i)) :
    (Pi.topologicalSpace : TopologicalSpace (∀ i, X i)) =
      ⨅ i, TopologicalSpace.induced (fun x ↦ x i) (T_X i) :=
  rfl

以上でMathlibが位相空間をより関手的な理論であり，任意の固定された型に対して完備束構造を持つことで，距離空間の理論の欠点を埋めようとする思想についてのツアーを終了します．

10.3.2. 分離公理と可算公理

位相空間の圏には非常に優れた性質があることを見てきました．その代償として，かなり病的な位相空間が存在します．位相空間には，その振る舞いが距離空間の振る舞いに近くなるようにするための仮定がいくつか存在します．最も重要なものは T2Space で，これは「ハウスドルフ性」とも呼ばれ，極限が一意であることを保証します．より強力な分離特性は T3Space で，これは RegularSpace の特性に加えて，各点が閉近傍の基底を持つことを保証します．

example [TopologicalSpace X] [T2Space X] {u : ℕ → X} {a b : X} (ha : Tendsto u atTop (𝓝 a))
    (hb : Tendsto u atTop (𝓝 b)) : a = b :=
  tendsto_nhds_unique ha hb

example [TopologicalSpace X] [RegularSpace X] (a : X) :
    (𝓝 a).HasBasis (fun s : Set X ↦ s ∈ 𝓝 a ∧ IsClosed s) id :=
  closed_nhds_basis a

どの位相空間においても，定義上，各点は開近傍の基底を持つことに注意してください．

example [TopologicalSpace X] {x : X} :
    (𝓝 x).HasBasis (fun t : Set X ↦ t ∈ 𝓝 x ∧ IsOpen t) id :=
  nhds_basis_opens' x

ここでの主な目的は，連続性による拡張を可能にする基本定理を証明することです．ブルバキのgeneral topologyの本，1.8.5，定理1より（自明でない含意のみをとります）：

\(X\) を位相空間， \(A\) を \(X\) の稠密部分集合， \(f : A → Y\) を \(A\) から \(T_3\) 空間 \(Y\) への連続写像とする．もし， \(X\) 内の各 \(x\) に対して， \(y\) が \(A\) に留まりながら \(x\) に限りなく近づく時に \(f(y)\) が \(Y\) 内の極限に収束するならば， \(f\) を \(X\) に連続に拡張した \(φ\) が存在する．

実際には，Mathlibには上記の補題のより一般的なバージョンである DenseInducing.continuousAt_extend が含まれていますが，ここではブルバキのバージョンにこだわることにします．

A : Set X が与えられると， ↥A は A に関連する部分型であり，Leanは必要な時は自動的にこのちょっと変な上向き矢印を挿入することを覚えておいてください．そして，この（包含な）型強制の対応は (↑) : A → X です．「 \(A\) に留まりながら \(x\) に限りなく近づく」という仮定は引き戻しのフィルタ comap (↑) (𝓝 x) に対応します．

まず文脈を簡単にするために抽出した補助的な補題を証明しましょう．（特にここではYが位相空間である必要はありません）．

theorem aux {X Y A : Type*} [TopologicalSpace X] {c : A → X}
      {f : A → Y} {x : X} {F : Filter Y}
      (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) :
    ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := by
  sorry

それでは，連続性定理による拡張のメインの証明に移りましょう．

Leanが ↥A 上の位相を必要とする場合，自動的に誘導位相を使用します．関連する唯一の補題は， nhds_induced (↑) : ∀ a : ↥A, 𝓝 a = comap (↑) (𝓝 ↑a) です（これは実際には誘導位相に関する一般的な補題です）．

証明の概要は以下のようになります：

メインの仮定と選択公理から， ∀ x, Tendsto f (comap (↑) (𝓝 x)) (𝓝 (φ x)) となる関数 φ が与えられます．（ Y はハウスドルフであるため， φ は完全に決定されますが， φ が実際に f を拡張することを証明するまではこの性質は必要ありません）．

まず φ が連続であることを証明しましょう．任意の x : X を固定します． Y は正則であるので， φ x の 閉 近傍 V' に対して， φ ⁻¹' V' ∈ 𝓝 x が成り立つことを確認すれば十分です．極限の仮定は（上の補助的な補題によって） IsOpen V ∧ (↑) ⁻¹' V ⊆ f ⁻¹' V' を満たす V ∈ 𝓝 x を与えます． V ∈ 𝓝 x であるため， V ⊆ φ ⁻¹' V' ，すなわち ∀ y ∈ V, φ y ∈ V' を証明すれば十分です．ここで V の要素 y を固定しましょう． V は 開 であるため， y の近傍です．特に (↑) ⁻¹' V ∈ comap (↑) (𝓝 y) となり，また f ⁻¹' V' ∈ comap (↑) (𝓝 y) となります．さらに A は稠密であるため， comap (↑) (𝓝 y) ≠ ⊥ です．そして Tendsto f (comap (↑) (𝓝 y)) (𝓝 (φ y)) は既知であるため， φ y ∈ closure V' が導かれ， V' が閉じていることから φ y ∈ V' が証明されたことになります．

あとは φ が f から拡張されていることを証明するだけです．これは Y がハウスドルフであるという事実とともに， f の連続性が議論に出てきます．

example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X}
    (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : Continuous f)
    (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) (𝓝 x)) (𝓝 c)) :
    ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := by
  sorry

#check HasBasis.tendsto_right_iff

分離の性質に加えて，位相空間を距離空間に近づけるための主な仮定として，可算性の仮定があります．主なものは第一可算で，これはすべての点が可算な基本近傍を持つことを求めるものです．特にこれは，集合の閉包が数列を使って理解できることを保証します．

example [TopologicalSpace X] [FirstCountableTopology X]
      {s : Set X} {a : X} :
    a ∈ closure s ↔ ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ Tendsto u atTop (𝓝 a) :=
  mem_closure_iff_seq_limit

10.3.3. コンパクト性

ここで，位相空間におけるコンパクト性の定義について説明しましょう．一般的に，コンパクト性にはいくつかの考え方がありますが，Mathlibではフィルターを用いたバージョンを使うことにしています．

まず，フィルターの集積点を定義する必要があります．位相空間 X 上のフィルター F が与えられたとき，点 x : X が F の集積点であるとは，一般化された集合として見た F と x に近い点の一般化された集合の共通部分が空でないことです．

したがって，集合 s は， s に含まれるすべての空でない一般化された集合 F ，つまり F ≤ 𝓟 s が s に集積点を持つとき，コンパクトであると言うことができます．

variable [TopologicalSpace X]

example {F : Filter X} {x : X} : ClusterPt x F ↔ NeBot (𝓝 x ⊓ F) :=
  Iff.rfl

example {s : Set X} :
    IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F :=
  Iff.rfl

例えば，F が map u atTop であり， atTop の u : ℕ → X による像，つまり一般化された非常に大きな自然数の集合であるとすると， F ≤ 𝓟 s という仮定は， n が十分な大きさであれば u n が s に属することを意味します． x が map u atTop の集積点であるということは，非常に大きな数による像が x に近い点の集合と交差していることを意味します． 𝓝 x が可算基底を持つ場合，これは u が x に収束する部分列を持つと解釈することができ，距離空間におけるコンパクト性がどのようなものかを再現することができます．

example [FirstCountableTopology X] {s : Set X} {u : ℕ → X} (hs : IsCompact s)
    (hu : ∀ n, u n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) :=
  hs.tendsto_subseq hu

集積点は連続写像に対して非常によくふるまいます．

variable [TopologicalSpace Y]

example {x : X} {F : Filter X} {G : Filter Y} (H : ClusterPt x F) {f : X → Y}
    (hfx : ContinuousAt f x) (hf : Tendsto f F G) : ClusterPt (f x) G :=
  ClusterPt.map H hfx hf

演習として，連続写像の下のコンパクト集合の像がコンパクトであることを証明しましょう．すでに見たことに加えて， Filter.push_pull と NeBot.of_map を使う必要があります．

example [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsCompact s) :
    IsCompact (f '' s) := by
  intro F F_ne F_le
  have map_eq : map f (𝓟 s ⊓ comap f F) = 𝓟 (f '' s) ⊓ F := by sorry
  have Hne : (𝓟 s ⊓ comap f F).NeBot := by sorry
  have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s := inf_le_left
  sorry

また，開集合の被覆という観点からコンパクト性を表現することもできます：もし s をカバーするすべての開集合の族が有限被覆の部分族を持つならば， s はコンパクトです．

example {ι : Type*} {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i))
    (hsU : s ⊆ ⋃ i, U i) : ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i :=
  hs.elim_finite_subcover U hUo hsU