11. Topologi

Kalkulus didasarkan pada konsep fungsi, yang digunakan untuk memodelkan besaran-besaran yang saling bergantung. Sebagai contoh, kita lazim mempelajari besaran yang berubah seiring waktu. Gagasan limit juga bersifat mendasar. Kita dapat mengatakan bahwa limit sebuah fungsi \(f(x)\) adalah nilai \(b\) ketika \(x\) mendekati nilai \(a\), atau bahwa \(f(x)\) konvergen ke \(b\) ketika \(x\) mendekati \(a\). Secara ekuivalen, kita dapat mengatakan bahwa \(f(x)\) mendekati \(b\) ketika \(x\) mendekati nilai \(a\), atau bahwa fungsi itu menuju \(b\) ketika \(x\) menuju \(a\). Kita telah mulai membahas gagasan-gagasan semacam ini dalam Bab 3.6.

Topologi adalah kajian abstrak tentang limit dan kekontinuan. Setelah membahas pokok-pokok formalisasi dalam Bab 2 hingga 7, dalam bab ini kita akan menjelaskan cara gagasan topologis diformalkan di Mathlib. Abstraksi topologis tidak hanya berlaku jauh lebih umum, tetapi, agak paradoksal, juga mempermudah penalaran tentang limit dan kekontinuan dalam contoh-contoh konkret.

Gagasan topologis dibangun di atas cukup banyak lapisan struktur matematika. Lapisan pertama adalah teori himpunan naif, sebagaimana dijelaskan dalam Bab 4. Lapisan berikutnya adalah teori filter, yang akan kita uraikan dalam Bab 11.1. Di atasnya kita susun teori ruang topologi, ruang metrik, dan sebuah gagasan antara yang sedikit lebih eksotis, yang disebut ruang seragam.

Bab-bab sebelumnya bertumpu pada gagasan matematika yang kemungkinan besar sudah Anda kenal, sedangkan gagasan filter kurang dikenal, bahkan oleh banyak matematikawan profesional. Namun, gagasan ini sangat penting agar matematika dapat diformalkan secara efektif. Mari kita jelaskan alasannya. Ambil sembarang fungsi f : ℝ → ℝ. Kita dapat meninjau limit f x ketika x mendekati suatu nilai x₀, tetapi kita juga dapat meninjau limit f x ketika x menuju tak hingga atau minus tak hingga. Kita juga dapat meninjau limit f x ketika x mendekati x₀ dari kanan, yang secara konvensional ditulis x₀⁺, atau dari kiri, yang ditulis x₀⁻. Ada pula variasi ketika x mendekati x₀, x₀⁺, atau x₀⁻, tetapi tidak boleh mengambil nilai x₀ itu sendiri. Dengan demikian, sedikitnya ada delapan cara bagi x untuk mendekati sesuatu. Kita juga dapat membatasi x pada nilai rasional atau memberlakukan syarat lain pada domainnya, tetapi kita cukup membahas delapan kasus tersebut.

Pada kodomain terdapat ragam pilihan yang serupa: kita dapat menentukan bahwa f x mendekati suatu nilai dari kiri atau kanan, atau bahwa nilainya menuju plus atau minus tak hingga, dan seterusnya. Sebagai contoh, kita mungkin ingin menyatakan bahwa f x menuju +∞ ketika x mendekati x₀ dari kanan tanpa sama dengan x₀. Hal ini menghasilkan 64 jenis pernyataan limit yang berbeda, padahal kita bahkan belum mulai menangani limit barisan seperti yang kita lakukan dalam Bab 3.6.

Masalahnya menjadi jauh lebih rumit lagi ketika kita mempertimbangkan lema-lema pendukung. Sebagai contoh, limit dapat dikomposisikan: jika f x menuju y₀ ketika x menuju x₀ dan g y menuju z₀ ketika y menuju y₀, maka g ∘ f x menuju z₀ ketika x menuju x₀. Ada tiga gagasan “menuju” yang berperan di sini, dan masing-masing dapat diinstansiasi dengan salah satu dari delapan cara yang dijelaskan dalam paragraf sebelumnya. Hasilnya adalah 512 lema—jumlah yang sangat besar untuk ditambahkan ke sebuah pustaka! Secara informal, matematikawan biasanya membuktikan dua atau tiga di antaranya, lalu sekadar mencatat bahwa sisanya dapat dibuktikan “dengan cara yang sama”. Formalisasi matematika menuntut agar gagasan “sama” yang relevan dibuat sepenuhnya eksplisit, dan tepat itulah yang berhasil dilakukan oleh teori filter Bourbaki.

11.1. Filter

Sebuah filter pada tipe X adalah koleksi himpunan bagian dari X yang memenuhi tiga syarat yang akan kita uraikan di bawah. Gagasan ini mendukung dua ide yang saling berkaitan:

• limit, termasuk semua jenis limit yang dibahas di atas: limit hingga dan tak hingga dari barisan, limit hingga dan tak hingga dari fungsi pada suatu titik atau di tak hingga, dan seterusnya.

• hal-hal yang pada akhirnya berlaku, termasuk hal-hal yang berlaku untuk n : ℕ yang cukup besar, cukup dekat dengan suatu titik x, untuk pasangan titik yang cukup berdekatan, atau hampir di mana-mana dalam pengertian teori ukuran. Secara dual, filter juga dapat mengungkapkan gagasan hal-hal yang sering berlaku: untuk n sebesar apa pun, pada suatu titik di setiap lingkungan dari titik tertentu, dan seterusnya.

Filter-filter yang sesuai dengan deskripsi ini akan didefinisikan nanti dalam bagian ini, tetapi kita sudah dapat menyebutkan namanya:

• (atTop : Filter ℕ), yang terdiri dari himpunan bagian ℕ yang memuat {n | n ≥ N} untuk suatu N

• 𝓝 x, yang terdiri dari lingkungan-lingkungan x dalam ruang topologi

• 𝓤 X, yang terdiri dari entourage suatu ruang seragam (ruang seragam memperumum ruang metrik dan grup topologis)

• μ.ae, yang terdiri dari himpunan-himpunan yang komplemennya berukuran nol terhadap suatu ukuran μ.

Definisi umumnya adalah sebagai berikut: filter F : Filter X adalah koleksi himpunan F.sets : Set (Set X) yang memenuhi syarat berikut:

• 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.

Syarat pertama menyatakan bahwa himpunan semua elemen X termasuk dalam F.sets. Syarat kedua menyatakan bahwa jika U termasuk dalam F.sets, maka setiap himpunan yang memuat U juga termasuk dalam F.sets. Syarat ketiga menyatakan bahwa F.sets tertutup terhadap irisan berhingga. Di Mathlib, filter F didefinisikan sebagai struktur yang membundel F.sets beserta ketiga sifatnya, tetapi sifat-sifat tersebut tidak membawa data tambahan, dan kita akan lebih mudah bekerja jika mengaburkan perbedaan antara F dan F.sets. Karena itu, kita mendefinisikan U ∈ F agar berarti U ∈ F.sets. Inilah sebabnya kata sets muncul dalam nama beberapa lema yang menyebut U ∈ F.

Mungkin membantu jika filter dipandang sebagai sesuatu yang mendefinisikan gagasan himpunan yang “cukup besar”. Syarat pertama lalu menyatakan bahwa univ cukup besar; syarat kedua menyatakan bahwa himpunan yang memuat himpunan yang cukup besar juga cukup besar; dan syarat ketiga menyatakan bahwa irisan dua himpunan yang cukup besar tetap cukup besar.

Mungkin lebih bermanfaat lagi jika filter pada tipe X dipandang sebagai elemen tergeneralisasi dari Set X. Sebagai contoh, atTop adalah “himpunan bilangan yang sangat besar” dan 𝓝 x₀ adalah “himpunan titik yang sangat dekat dengan x₀”. Salah satu perwujudan sudut pandang ini ialah bahwa kita dapat mengaitkan setiap s : Set X dengan apa yang disebut filter utama, yang terdiri dari semua himpunan yang memuat s. Definisi ini sudah tersedia di Mathlib dan memiliki notasi 𝓟 (yang dilokalkan dalam namespace Filter). Sebagai demonstrasi, gunakan kesempatan ini untuk menyusun sendiri definisinya.

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

Untuk contoh kedua, kami meminta Anda mendefinisikan filter atTop : Filter ℕ. (Kita dapat menggunakan tipe apa pun yang memiliki praorder sebagai pengganti ℕ.)

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

Kita juga dapat langsung mendefinisikan filter lingkungan 𝓝 x₀ bagi sembarang x₀ : ℝ. Pada bilangan real, lingkungan x₀ adalah himpunan yang memuat interval terbuka \((x_0 - \varepsilon, x_0 + \varepsilon)\), yang didefinisikan di Mathlib sebagai Ioo (x₀ - ε) (x₀ + ε). (Gagasan lingkungan ini hanyalah kasus khusus dari konstruksi yang lebih umum di Mathlib.)

Dengan contoh-contoh ini, kita sudah dapat mendefinisikan apa artinya fungsi f : X → Y konvergen ke suatu G : Filter Y sepanjang suatu F : Filter X, sebagai berikut:

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

Jika X adalah ℕ dan Y adalah ℝ, maka Tendsto₁ u atTop (𝓝 x) ekuivalen dengan pernyataan bahwa barisan u : ℕ → ℝ konvergen ke bilangan real x. Jika X dan Y sama-sama ℝ, maka Tendsto f (𝓝 x₀) (𝓝 y₀) ekuivalen dengan gagasan yang sudah akrab, \(\lim_{x \to x₀} f(x) = y₀\). Semua jenis limit lain yang disebutkan dalam pendahuluan juga ekuivalen dengan instans Tendsto₁ untuk pilihan filter sumber dan target yang sesuai.

Gagasan Tendsto₁ di atas ekuivalen secara definisional dengan gagasan Tendsto yang didefinisikan di Mathlib, tetapi definisi yang kedua lebih abstrak. Masalah pada definisi Tendsto₁ ialah bahwa definisi tersebut menampilkan kuantor dan elemen-elemen G, serta menyembunyikan intuisi yang diperoleh dengan memandang filter sebagai himpunan tergeneralisasi. Kita dapat menyembunyikan kuantor ∀ V dan lebih menonjolkan intuisi itu dengan memakai perangkat aljabar dan teori himpunan yang lebih kaya. Bahan pertama adalah operasi pendorongan maju (pushforward) \(f_*\) yang dikaitkan dengan setiap pemetaan f : X → Y dan dinotasikan sebagai Filter.map f di Mathlib. Untuk filter F pada X, Filter.map f F : Filter Y didefinisikan sedemikian rupa sehingga V ∈ Filter.map f F ↔ f ⁻¹' V ∈ F berlaku secara definisional. Dalam berkas contoh, kita telah membuka namespace Filter sehingga Filter.map dapat ditulis sebagai map. Dengan demikian, kita dapat menulis ulang definisi Tendsto menggunakan relasi urutan pada Filter Y, yaitu inklusi terbalik dari himpunan para anggotanya. Dengan kata lain, untuk G H : Filter Y, berlaku 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

Relasi urutan pada filter mungkin tampak terbalik. Namun, ingat bahwa filter pada X dapat dipandang sebagai elemen tergeneralisasi dari Set X melalui inklusi 𝓟 : Set X → Filter X, yang memetakan setiap himpunan s ke filter utama yang bersesuaian. Inklusi ini mempertahankan urutan, sehingga relasi urutan pada Filter memang dapat dipandang sebagai relasi inklusi alami antara himpunan tergeneralisasi. Dalam analogi ini, pendorongan maju serupa dengan citra langsung. Dan memang, map f (𝓟 s) = 𝓟 (f '' s).

Sekarang kita dapat memahami secara intuitif mengapa barisan u : ℕ → ℝ konvergen ke titik x₀ jika dan hanya jika berlaku map u atTop ≤ 𝓝 x₀. Ketaksamaan ini berarti bahwa “citra langsung melalui u” dari “himpunan bilangan asli yang sangat besar” “tercakup” dalam “himpunan titik yang sangat dekat dengan x₀”.

Sesuai janji, definisi Tendsto₂ tidak menampilkan kuantor ataupun himpunan. Definisi ini juga memanfaatkan sifat aljabar operasi pendorongan maju. Pertama, setiap Filter.map f bersifat monoton. Kedua, Filter.map kompatibel dengan komposisi.

#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)

Kedua sifat ini bersama-sama memungkinkan kita membuktikan bahwa limit dapat dikomposisikan. Sekaligus kita memperoleh seluruh 512 varian lema komposisi yang dijelaskan dalam pendahuluan, serta banyak hasil lainnya. Sebagai latihan, buktikan pernyataan berikut menggunakan definisi Tendsto₁ dalam bentuk kuantor universal atau menggunakan definisi aljabarnya, bersama dengan kedua lema di atas.

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

Konstruksi pendorongan maju menggunakan sebuah pemetaan untuk mendorong filter dari sumber pemetaan ke targetnya. Ada pula operasi penarikan balik (pullback), Filter.comap, yang bergerak ke arah sebaliknya. Operasi ini memperumum operasi prapeta pada himpunan. Untuk setiap pemetaan f, Filter.map f dan Filter.comap f membentuk apa yang dikenal sebagai koneksi Galois, artinya keduanya memenuhi

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

untuk setiap F dan G. Operasi ini dapat digunakan untuk memberikan formulasi lain bagi Tendsto yang dapat dibuktikan ekuivalen—tetapi tidak ekuivalen secara definisional—dengan formulasi di Mathlib.

Operasi comap dapat digunakan untuk membatasi filter pada suatu subtipe. Sebagai contoh, andaikan kita memiliki f : ℝ → ℝ, x₀ : ℝ, dan y₀ : ℝ, serta ingin menyatakan bahwa f x mendekati y₀ ketika x mendekati x₀ melalui bilangan rasional. Kita dapat menarik balik filter 𝓝 x₀ ke ℚ menggunakan pemetaan koersif (↑) : ℚ → ℝ dan menyatakan Tendsto (f ∘ (↑) : ℚ → ℝ) (comap (↑) (𝓝 x₀)) (𝓝 y₀).

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

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

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

Operasi penarikan balik juga kompatibel dengan komposisi, tetapi bersifat kontravarian, artinya operasi ini membalik urutan argumen.

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

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

end

Sekarang mari kita beralih ke bidang ℝ × ℝ dan mencoba memahami hubungan antara lingkungan titik (x₀, y₀) dengan 𝓝 x₀ dan 𝓝 y₀. Ada operasi produk Filter.prod : Filter X → Filter Y → Filter (X × Y), yang dinotasikan dengan ×ˢ dan menjawab pertanyaan ini:

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

Operasi produk didefinisikan menggunakan operasi penarikan balik dan operasi inf:

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

Di sini, operasi inf merujuk pada struktur kisi pada Filter X untuk sembarang tipe X; dalam struktur ini, F ⊓ G adalah filter terbesar yang lebih kecil daripada F dan G. Jadi, operasi inf memperumum gagasan irisan himpunan.

Banyak bukti di Mathlib menggunakan seluruh struktur yang disebutkan di atas (map, comap, inf, sup, dan prod) untuk memberikan bukti aljabar tentang konvergensi tanpa pernah merujuk pada anggota filter. Anda dapat berlatih melakukannya dalam bukti lema berikut, dengan menguraikan definisi Tendsto dan Filter.prod jika diperlukan.

#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

Tipe terurut Filter X sebenarnya merupakan kisi lengkap; artinya, terdapat elemen terbawah dan elemen teratas, serta setiap himpunan filter pada X memiliki Inf dan Sup.

Perhatikan bahwa dengan adanya sifat kedua dalam definisi filter (jika U termasuk dalam F, maka setiap himpunan yang lebih besar daripada U juga termasuk dalam F), sifat pertama (himpunan semua penghuni X termasuk dalam F) ekuivalen dengan sifat bahwa F bukan koleksi himpunan yang kosong. Hal ini jangan dikacaukan dengan pertanyaan yang lebih halus tentang apakah himpunan kosong merupakan elemen dari F. Definisi filter tidak melarang ∅ ∈ F, tetapi jika himpunan kosong berada dalam F, maka setiap himpunan berada dalam F; dengan kata lain, ∀ U : Set X, U ∈ F. Dalam kasus ini, F adalah filter yang terbilang trivial, tepatnya elemen terbawah dari kisi lengkap Filter X. Hal ini berbeda dengan definisi filter dalam Bourbaki, yang tidak mengizinkan filter yang memuat himpunan kosong.

Karena kita memasukkan filter trivial dalam definisi, terkadang kita perlu secara eksplisit mengasumsikan sifat nontrivial dalam beberapa lema. Sebagai imbalannya, teori yang dihasilkan memiliki sifat global yang lebih baik. Kita telah melihat bahwa memasukkan filter trivial memberikan elemen terbawah. Hal ini juga memungkinkan kita mendefinisikan principal : Set X → Filter X, yang memetakan ∅ ke ⊥, tanpa menambahkan prasyarat untuk mengecualikan himpunan kosong. Selain itu, kita juga dapat mendefinisikan operasi penarikan balik tanpa prasyarat. Memang, comap f F = ⊥ dapat terjadi meskipun F ≠ ⊥. Sebagai contoh, untuk x₀ : ℝ dan s : Set ℝ, penarikan balik 𝓝 x₀ melalui koersi dari subtipe yang bersesuaian dengan s bersifat nontrivial jika dan hanya jika x₀ termasuk dalam penutupan s.

Untuk menangani lema yang memang perlu mengasumsikan bahwa suatu filter bersifat nontrivial, Mathlib menyediakan kelas tipe Filter.NeBot, dan pustaka ini memiliki lema-lema yang mengasumsikan (F : Filter X) [F.NeBot]. Sebagai contoh, basis data instans mengetahui bahwa (atTop : Filter ℕ).NeBot dan bahwa mendorong maju filter nontrivial menghasilkan filter nontrivial. Akibatnya, lema yang mengasumsikan [F.NeBot] akan otomatis berlaku pada map u atTop untuk setiap barisan u.

Peninjauan kita atas sifat aljabar filter dan hubungannya dengan limit pada dasarnya telah selesai, tetapi kita belum membenarkan klaim bahwa gagasan limit yang lazim telah berhasil diperoleh kembali. Sepintas, Tendsto u atTop (𝓝 x₀) mungkin tampak lebih kuat daripada gagasan konvergensi yang didefinisikan dalam Bab 3.6, sebab kita mensyaratkan agar setiap lingkungan x₀ memiliki prapeta yang termasuk dalam atTop, sedangkan definisi biasa hanya mensyaratkannya untuk lingkungan standar Ioo (x₀ - ε) (x₀ + ε). Kuncinya ialah bahwa menurut definisi, setiap lingkungan memuat lingkungan standar semacam itu. Pengamatan ini mengantar kita pada gagasan basis filter.

Untuk F : Filter X, keluarga himpunan s : ι → Set X merupakan basis bagi F jika, untuk setiap himpunan U, berlaku U ∈ F jika dan hanya jika himpunan tersebut memuat suatu s i. Dengan kata lain, secara formal s adalah basis jika memenuhi ∀ U : Set X, U ∈ F ↔ ∃ i, s i ⊆ U. Kita memperoleh keluwesan lebih besar lagi dengan mempertimbangkan predikat pada ι yang hanya memilih sebagian nilai i dalam tipe indeks. Dalam kasus 𝓝 x₀, kita ingin ι berupa ℝ, menulis ε sebagai pengganti i, dan menggunakan predikat yang memilih nilai positif ε. Jadi, fakta bahwa himpunan Ioo (x₀ - ε) (x₀ + ε) membentuk basis bagi topologi lingkungan pada ℝ dinyatakan sebagai berikut:

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

Filter atTop juga memiliki basis yang nyaman. Dengan lema Filter.HasBasis.tendsto_iff, kita dapat merumuskan ulang pernyataan berbentuk Tendsto f F G jika basis bagi F dan G diketahui. Dengan menyatukan semua bagian ini, pada dasarnya kita memperoleh gagasan konvergensi yang digunakan dalam Bab 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

Sekarang kita tunjukkan bagaimana filter memudahkan kita bekerja dengan sifat yang berlaku untuk bilangan yang cukup besar atau untuk titik yang cukup dekat dengan suatu titik tertentu. Dalam Bab 3.6, kita sering menghadapi keadaan ketika diketahui bahwa sifat P n berlaku untuk n yang cukup besar dan sifat lain Q n juga berlaku untuk n yang cukup besar. Dengan menggunakan cases dua kali, kita memperoleh N_P dan N_Q yang memenuhi ∀ n ≥ N_P, P n dan ∀ n ≥ N_Q, Q n. Setelah menggunakan set N := max N_P N_Q, pada akhirnya kita dapat membuktikan ∀ n ≥ N, P n ∧ Q n. Melakukannya berulang kali terasa melelahkan.

Kita dapat bekerja lebih baik dengan memperhatikan bahwa pernyataan “P n dan Q n berlaku untuk n yang cukup besar” berarti bahwa kita memiliki {n | P n} ∈ atTop dan {n | Q n} ∈ atTop. Karena atTop adalah filter, irisan dua elemen atTop juga termasuk dalam atTop, sehingga berlaku {n | P n ∧ Q n} ∈ atTop. Menulis {n | P n} ∈ atTop terasa kurang nyaman, tetapi kita dapat menggunakan notasi yang lebih sugestif, ∀ᶠ n in atTop, P n. Huruf f yang ditulis sebagai superskrip di sini adalah singkatan dari “Filter”. Anda dapat memahami notasi tersebut sebagai pernyataan bahwa untuk semua n dalam “himpunan bilangan yang sangat besar”, P n berlaku. Notasi ∀ᶠ merupakan singkatan dari Filter.Eventually, dan lema Filter.Eventually.and menggunakan sifat irisan filter untuk melakukan persis apa yang baru saja kita uraikan:

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

Notasi ini begitu nyaman dan intuitif sehingga tersedia pula spesialisasi ketika P merupakan pernyataan kesamaan atau ketaksamaan. Sebagai contoh, ambil dua barisan bilangan real u dan v. Kita akan menunjukkan bahwa jika u n dan v n berimpit untuk n yang cukup besar, maka u menuju x₀ jika dan hanya jika v menuju x₀. Pertama kita akan memakai Eventually yang generik, kemudian versi yang dikhususkan bagi predikat kesamaan, yaitu EventuallyEq. Kedua pernyataan ini ekuivalen secara definisional sehingga bukti yang sama berlaku pada kedua kasus.

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

Ada gunanya kita meninjau kembali definisi filter dalam kerangka Eventually. Untuk F : Filter X dan sembarang predikat P serta Q pada X,

• syarat univ ∈ F menjamin (∀ x, P x) → ∀ᶠ x in F, P x,

• syarat U ∈ F → U ⊆ V → V ∈ F menjamin (∀ᶠ x in F, P x) → (∀ x, P x → Q x) → ∀ᶠ x in F, Q x, dan

• syarat U ∈ F → V ∈ F → U ∩ V ∈ F menjamin (∀ᶠ 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

Butir kedua, yang bersesuaian dengan Eventually.mono, menyediakan cara yang nyaman untuk menggunakan filter, terutama jika digabungkan dengan Eventually.and. Taktik filter_upwards memungkinkan kita menggabungkan keduanya. Bandingkan:

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'⟩

Pembaca yang mengenal teori ukuran akan memperhatikan bahwa filter μ.ae yang terdiri dari himpunan-himpunan berkomplemen ukuran nol (alias “himpunan yang terdiri dari hampir setiap titik”) tidak terlalu berguna sebagai sumber atau target Tendsto. Namun, filter ini dapat digunakan dengan mudah bersama Eventually untuk menyatakan bahwa suatu sifat berlaku pada hampir setiap titik.

Terdapat versi dual dari ∀ᶠ x in F, P x yang kadang-kadang berguna: ∃ᶠ x in F, P x berarti {x | ¬P x} ∉ F. Sebagai contoh, ∃ᶠ n in atTop, P n berarti terdapat n sebesar apa pun yang memenuhi P n. Notasi ∃ᶠ merupakan singkatan dari Filter.Frequently.

Sebagai contoh yang lebih canggih, pertimbangkan pernyataan berikut tentang barisan u, himpunan M, dan nilai x:

Jika u konvergen ke x dan u n termasuk dalam M untuk n yang cukup besar, maka x berada dalam penutupan M.

Pernyataan ini dapat diformalkan sebagai berikut:

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

Ini adalah kasus khusus dari teorema mem_closure_of_tendsto dalam pustaka topologi. Cobalah membuktikannya menggunakan lema-lema yang dikutip, dengan memanfaatkan fakta bahwa ClusterPt x F berarti (𝓝 x ⊓ F).NeBot dan bahwa, menurut definisi, asumsi ∀ᶠ n in atTop, u n ∈ M berarti 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

11.2. Ruang metrik

Contoh-contoh pada bagian sebelumnya berfokus pada barisan bilangan real. Dalam bagian ini kita akan sedikit meningkatkan keumumannya dan berfokus pada ruang metrik. Ruang metrik adalah tipe X yang dilengkapi fungsi jarak dist : X → X → ℝ, yang memperumum fungsi fun x y ↦ |x - y| dari kasus X = ℝ.

Mendeklarasikan ruang semacam ini mudah, dan kita akan memeriksa semua sifat yang disyaratkan bagi fungsi jaraknya.

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)

Perhatikan bahwa tersedia pula varian yang jaraknya dapat bernilai tak hingga, varian yang memungkinkan dist a b bernilai nol tanpa a = b, serta varian yang memiliki kedua sifat tersebut. Masing-masing disebut EMetricSpace, PseudoMetricSpace, dan PseudoEMetricSpace (huruf “e” di sini merupakan singkatan dari “extended”, atau diperluas).

Perhatikan bahwa perjalanan kita dari ℝ menuju ruang metrik melewati kasus khusus ruang bernorma, yang juga memerlukan aljabar linear dan akan dijelaskan sebagai bagian dari bab kalkulus.

11.2.1. Konvergensi dan kekontinuan

Dengan fungsi jarak, kita sudah dapat mendefinisikan barisan konvergen dan fungsi kontinu antar-ruang metrik. Keduanya sebenarnya didefinisikan dalam tatanan yang lebih umum, yang akan dibahas pada bagian berikutnya, tetapi tersedia lema yang merumuskan ulang definisinya dalam kerangka jarak.

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

Banyak sekali lema memiliki asumsi kekontinuan. Karena itu, kita akan sering membuktikan hasil kekontinuan, dan tersedia taktik continuity yang dikhususkan untuk tugas tersebut. Mari kita buktikan sebuah pernyataan kekontinuan yang akan diperlukan dalam latihan di bawah. Perhatikan bahwa Lean mengetahui cara memperlakukan produk dua ruang metrik sebagai ruang metrik; Lean memilih norma supremum, sehingga dist (x₁, y₁) (x₂, y₂) = max (dist x₁ x₂) (dist y₁ y₂) berlaku berdasarkan refleksivitas. Karena itu, masuk akal untuk mempertimbangkan fungsi kontinu dari X × X ke ℝ. Secara khusus, fungsi jarak dalam versi tanpa currying merupakan fungsi semacam itu.

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

Taktik ini agak lambat, sehingga berguna pula untuk mengetahui cara mengerjakannya secara manual. Pertama, kita perlu menggunakan fakta bahwa fun p : X × X ↦ f p.1 kontinu karena merupakan komposisi dari f, yang kontinu berdasarkan asumsi hf, dengan proyeksi Prod.fst, yang kekontinuannya dinyatakan oleh lema continuous_fst. Sifat komposisi adalah Continuous.comp. Karena sifat ini berada dalam namespace Continuous, kita dapat menggunakan notasi titik untuk meringkas Continuous.comp hf continuous_fst menjadi hf.comp continuous_fst. Bentuk yang kedua justru lebih mudah dibaca karena benar-benar terbaca sebagai komposisi asumsi kita dengan lema tersebut. Kita dapat melakukan hal yang sama pada komponen kedua untuk memperoleh kekontinuan fun p : X × X ↦ f p.2. Selanjutnya, kita gabungkan kedua hasil kekontinuan itu menggunakan Continuous.prodMk untuk memperoleh (hf.comp continuous_fst).prodMk (hf.comp continuous_snd) : Continuous (fun p : X × X ↦ (f p.1, f p.2)), lalu melakukan komposisi sekali lagi untuk mendapatkan bukti lengkap.

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).prodMk (hf.comp continuous_snd))

Kombinasi Continuous.prodMk dan continuous_dist melalui Continuous.comp terasa agak kikuk, bahkan jika kita banyak menggunakan notasi titik seperti di atas. Masalah yang lebih serius ialah bahwa bukti yang rapi ini memerlukan banyak perencanaan. Lean menerima term bukti di atas karena term itu merupakan term lengkap yang membuktikan pernyataan yang ekuivalen secara definisional dengan sasaran kita. Definisi penting yang perlu diuraikan di sini adalah definisi komposisi fungsi. Memang, fungsi sasaran kita fun p : X × X ↦ dist (f p.1) (f p.2) tidak disajikan sebagai komposisi. Term bukti yang kita berikan membuktikan kekontinuan dist ∘ (fun p : X × X ↦ (f p.1, f p.2)), yang kebetulan sama secara definisional dengan fungsi sasaran. Namun, jika kita mencoba membangun bukti ini secara bertahap dengan taktik yang dimulai dari apply continuous_dist.comp, elaborator Lean tidak akan mengenali komposisinya dan akan menolak menerapkan lema tersebut. Elaborator terutama kesulitan ketika produk tipe terlibat.

Lema yang lebih baik untuk diterapkan di sini adalah Continuous.dist {f g : X → Y} : Continuous f → Continuous g → Continuous (fun x ↦ dist (f x) (g x)) yang lebih mudah ditangani elaborator Lean dan juga menghasilkan bukti lebih pendek jika term bukti lengkap diberikan secara langsung. Hal ini terlihat dari dua bukti baru untuk pernyataan di atas:

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)

Perhatikan bahwa, tanpa masalah elaborasi yang timbul dari komposisi, cara lain untuk meringkas bukti kita adalah menggunakan Continuous.prod_map, yang terkadang berguna.

Karena sayang jika harus memilih antara versi yang lebih mudah dielaborasi dan versi yang lebih singkat diketik, mari kita akhiri pembahasan ini dengan satu peringkasan terakhir yang ditawarkan oleh Continuous.fst'. Lema ini memungkinkan kita meringkas hf.comp continuous_fst menjadi hf.fst' (dan hal yang sama berlaku bagi snd), sehingga kita memperoleh bukti terakhir yang kini hampir menjadi terlalu tersamar.

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'

Sekarang giliran Anda membuktikan sebuah lema kekontinuan. Setelah mencoba taktik continuity, Anda akan memerlukan Continuous.add, continuous_pow, dan continuous_id untuk mengerjakannya secara manual.

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

Sejauh ini kita memandang kekontinuan sebagai gagasan global, tetapi kekontinuan pada suatu titik juga dapat didefinisikan.

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

11.2.2. Bola, himpunan terbuka, dan himpunan tertutup

Setelah memiliki fungsi jarak, definisi geometris terpenting adalah bola (terbuka) dan bola tertutup.

variable (r : ℝ)

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

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

Perhatikan bahwa r di sini merupakan sembarang bilangan real; tidak ada batasan tanda. Tentu saja, beberapa pernyataan memang mensyaratkan kondisi pada jari-jarinya.

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

Setelah memiliki bola, kita dapat mendefinisikan himpunan terbuka. Himpunan terbuka sebenarnya didefinisikan dalam tatanan yang lebih umum, yang dibahas pada bagian berikutnya, tetapi tersedia lema yang merumuskan ulang definisinya dalam kerangka bola.

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

Selanjutnya, himpunan tertutup adalah himpunan yang komplemennya terbuka. Sifat pentingnya ialah bahwa himpunan tertutup tetap tertutup terhadap pengambilan limit. Penutupan suatu himpunan adalah himpunan tertutup terkecil yang memuatnya.

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

Kerjakan latihan berikut tanpa menggunakan mem_closure_iff_seq_limit.

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

Ingat dari bagian tentang filter bahwa filter lingkungan memainkan peran besar di Mathlib. Dalam konteks ruang metrik, pokok pentingnya ialah bahwa bola menyediakan basis bagi filter tersebut. Lema utama di sini adalah Metric.nhds_basis_ball dan Metric.nhds_basis_closedBall, yang menyatakan hal ini untuk bola terbuka dan tertutup berjari-jari positif. Titik pusat merupakan argumen implisit, sehingga kita dapat memanggil Filter.HasBasis.mem_iff seperti dalam contoh berikut.

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

11.2.3. Kekompakan

Kekompakan adalah gagasan topologis yang penting. Gagasan ini membedakan himpunan bagian ruang metrik yang memiliki sifat serupa dengan ruas pada bilangan real, dibandingkan dengan interval lainnya:

• Setiap barisan yang nilainya berada dalam himpunan kompak memiliki subbarisan yang konvergen di dalam himpunan tersebut.

• Setiap fungsi kontinu pada himpunan kompak tak-kosong yang bernilai bilangan real bersifat terbatas dan mencapai batas bawah maupun batas atasnya di suatu titik (hasil ini disebut teorema nilai ekstrem).

• Himpunan kompak merupakan himpunan tertutup.

Pertama, mari kita periksa bahwa interval satuan pada bilangan real memang merupakan himpunan kompak, lalu periksa klaim-klaim di atas bagi himpunan kompak dalam ruang metrik umum. Pada pernyataan kedua, kita hanya memerlukan kekontinuan pada himpunan yang diberikan, sehingga kita akan menggunakan ContinuousOn sebagai pengganti Continuous dan memberikan pernyataan terpisah bagi minimum dan maksimum. Tentu saja, semua hasil ini diturunkan dari versi yang lebih umum, beberapa di antaranya akan dibahas pada bagian-bagian berikutnya.

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

Kita juga dapat menyatakan bahwa sebuah ruang metrik kompak secara global dengan menggunakan kelas tipe tambahan yang bernilai Prop:

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

Dalam ruang metrik kompak, setiap himpunan tertutup bersifat kompak; hasil ini adalah IsClosed.isCompact.

11.2.4. Fungsi kontinu seragam

Sekarang kita beralih ke gagasan keseragaman pada ruang metrik: fungsi kontinu seragam, barisan Cauchy, dan kelengkapan. Sekali lagi, semua gagasan tersebut didefinisikan dalam konteks yang lebih umum, tetapi tersedia lema dalam namespace metrik untuk mengakses definisi elementernya. Kita mulai dengan kekontinuan seragam.

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

Untuk berlatih memanipulasi semua definisi tersebut, kita akan membuktikan bahwa fungsi kontinu dari ruang metrik kompak ke ruang metrik bersifat kontinu seragam (kita akan melihat versi yang lebih umum pada bagian selanjutnya).

Pertama, kita berikan sketsa informal. Misalkan f : X → Y adalah fungsi kontinu dari ruang metrik kompak ke ruang metrik. Kita tetapkan ε > 0 dan mulai mencari suatu δ.

Tetapkan φ : X × X → ℝ := fun p ↦ dist (f p.1) (f p.2) dan K := { p : X × X | ε ≤ φ p }. Perhatikan bahwa φ kontinu karena f dan fungsi jarak kontinu. Selain itu, K jelas tertutup (gunakan isClosed_le), sehingga kompak karena X kompak dan Lean mengetahui bahwa produk ruang kompak juga kompak.

Kemudian kita membahas dua kemungkinan dengan menggunakan eq_empty_or_nonempty. Jika K kosong, jelas kita telah selesai (misalnya, kita dapat menetapkan δ = 1). Jadi, andaikan K tidak kosong. Gunakan teorema nilai ekstrem untuk memilih (x₀, x₁) yang mencapai infimum fungsi jarak pada K. Selanjutnya, kita dapat menetapkan δ = dist x₀ x₁ dan memeriksa bahwa semuanya berlaku.

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

11.2.5. Kelengkapan

Barisan Cauchy dalam ruang metrik adalah barisan yang suku-sukunya semakin saling mendekat. Ada beberapa cara ekuivalen untuk menyatakan gagasan ini. Secara khusus, barisan konvergen merupakan barisan Cauchy. Kebalikannya hanya berlaku dalam ruang yang disebut lengkap.

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

Kita akan berlatih menggunakan definisi ini dengan membuktikan sebuah kriteria praktis yang merupakan kasus khusus dari kriteria di Mathlib. Ini juga kesempatan baik untuk berlatih menggunakan jumlah besar dalam konteks geometris. Selain penjelasan dari bagian tentang filter, Anda mungkin memerlukan tendsto_pow_atTop_nhds_zero_of_lt_one, Tendsto.mul, dan 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  ∈ range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
    _ ≤ ∑ i  ∈ range k, (1 / 2 : ℝ) ^ (N + i) := sorry
    _ = 1 / 2 ^ N * ∑ i  ∈ range k, (1 / 2 : ℝ) ^ i := sorry
    _ ≤ 1 / 2 ^ N * 2 := sorry
    _ < ε := sorry

Kita siap menghadapi lawan terakhir pada bagian ini: teorema Baire untuk ruang metrik lengkap! Kerangka bukti di bawah memperlihatkan beberapa teknik menarik. Kerangka ini menggunakan varian bertanda seru dari taktik choose (cobalah menghapus tanda seru tersebut) dan menunjukkan cara mendefinisikan sesuatu secara induktif di tengah bukti menggunakan 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
  /- Ubah asumsi kerapatan menjadi dua fungsi `center` dan `radius` yang mengaitkan
    setiap n, x, δ, δpos dengan sebuah pusat dan jari-jari positif sedemikian sehingga
    `closedBall center radius` tercakup dalam `f n` sekaligus `closedBall x δ`.
    Kita juga dapat mensyaratkan `radius ≤ (1/2)^(n+1)` agar kelak memperoleh barisan Cauchy. -/
  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
  /- `ε` bernilai positif. Kita harus menemukan sebuah titik dalam bola berjari-jari `ε`
    di sekitar `x` yang termasuk dalam semua `f n`. Untuk itu, secara induktif kita
    bangun barisan `F n = (c n, r n)` sedemikian sehingga bola tertutup
    `closedBall (c n) (r n)` tercakup dalam bola sebelumnya sekaligus dalam `f n`,
    dan `r n` cukup kecil untuk menjamin bahwa `c n` adalah barisan Cauchy.
    Kemudian `c n` konvergen ke suatu limit yang termasuk dalam semua `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
  -- karena barisan `c n` bersifat Cauchy dalam ruang lengkap, barisan itu konvergen ke limit `y`.
  rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩
  -- titik `y` ini akan menjadi titik yang dicari. Kita akan memeriksa bahwa titik tersebut termasuk
  -- dalam semua `f n` dan dalam `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

11.3. Ruang topologi

11.3.1. Dasar-dasar

Sekarang kita meningkatkan keumuman dan memperkenalkan ruang topologi. Kita akan meninjau dua cara utama untuk mendefinisikan ruang topologi, lalu menjelaskan mengapa kategori ruang topologi memiliki perilaku yang jauh lebih baik daripada kategori ruang metrik. Perhatikan bahwa kita tidak akan menggunakan teori kategori Mathlib di sini; kita hanya mengambil sudut pandang yang agak kategoris.

Cara pertama untuk memikirkan peralihan dari ruang metrik ke ruang topologi ialah dengan hanya mengingat gagasan himpunan terbuka (atau, secara ekuivalen, gagasan himpunan tertutup). Dari sudut pandang ini, ruang topologi adalah tipe yang dilengkapi koleksi himpunan yang disebut himpunan terbuka. Koleksi tersebut harus memenuhi sejumlah aksioma yang disajikan di bawah (koleksi ini sedikit redundan, tetapi hal itu akan kita abaikan).

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

Himpunan tertutup kemudian didefinisikan sebagai himpunan yang komplemennya terbuka. Sebuah fungsi antar-ruang topologi bersifat kontinu (secara global) jika semua prapeta himpunan terbuka bersifat terbuka.

variable {Y : Type*} [TopologicalSpace Y]

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

Dengan definisi ini, kita sudah melihat bahwa dibandingkan dengan ruang metrik, ruang topologi hanya mengingat informasi secukupnya untuk membahas fungsi kontinu: dua struktur topologis pada suatu tipe sama jika dan hanya jika keduanya memiliki fungsi-fungsi kontinu yang sama (memang, fungsi identitas akan kontinu dalam kedua arah jika dan hanya jika kedua struktur memiliki himpunan terbuka yang sama).

Namun, begitu beralih ke kekontinuan pada suatu titik, kita melihat keterbatasan pendekatan berbasis himpunan terbuka. Di Mathlib, kita sering memandang ruang topologis sebagai tipe yang dilengkapi filter lingkungan 𝓝 x pada setiap titik x (fungsi yang bersesuaian, X → Filter X, memenuhi syarat tertentu yang dijelaskan lebih jauh di bawah). Ingat dari bagian tentang filter bahwa perangkat ini memainkan dua peran yang berkaitan. Pertama, 𝓝 x dipandang sebagai himpunan tergeneralisasi dari titik-titik X yang dekat dengan x. Kemudian, untuk setiap predikat P : X → Prop, filter tersebut menyediakan cara untuk menyatakan bahwa predikat itu berlaku pada titik yang cukup dekat dengan x. Mari kita nyatakan bahwa f : X → Y kontinu pada x. Cara yang murni menggunakan filter ialah menyatakan bahwa citra langsung melalui f dari himpunan tergeneralisasi titik-titik yang dekat dengan x tercakup dalam himpunan tergeneralisasi titik-titik yang dekat dengan f x. Ingat bahwa pernyataan ini ditulis sebagai map f (𝓝 x) ≤ 𝓝 (f x) atau Tendsto f (𝓝 x) (𝓝 (f x)).

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

Kita juga dapat merumuskannya dengan memandang lingkungan sebagai himpunan biasa dan filter lingkungan sebagai himpunan tergeneralisasi: “untuk setiap lingkungan U dari f x, semua titik yang dekat dengan x dipetakan ke U”. Perhatikan bahwa buktinya sekali lagi adalah Iff.rfl; sudut pandang ini ekuivalen secara definisional dengan sudut pandang sebelumnya.

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

Sekarang kita jelaskan cara beralih dari satu sudut pandang ke sudut pandang lainnya. Dalam kerangka himpunan terbuka, kita dapat mendefinisikan anggota 𝓝 x sebagai himpunan yang memuat suatu himpunan terbuka yang mengandung x.

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

Untuk bergerak ke arah sebaliknya, kita perlu membahas syarat yang harus dipenuhi 𝓝 : X → Filter X agar menjadi fungsi lingkungan suatu topologi.

Syarat pertama ialah bahwa 𝓝 x, jika dipandang sebagai himpunan tergeneralisasi, memuat himpunan {x} yang dipandang sebagai himpunan tergeneralisasi pure x (menjelaskan nama yang aneh ini akan membawa kita terlalu jauh menyimpang, jadi untuk sementara kita terima saja). Dengan kata lain, jika sebuah predikat berlaku pada titik-titik yang dekat dengan x, maka predikat tersebut berlaku pada 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

Syarat berikutnya lebih halus: untuk setiap predikat P : X → Prop dan setiap x, jika P y berlaku bagi y yang dekat dengan x, maka bagi y yang dekat dengan x dan z yang dekat dengan y, berlaku P z. Lebih tepatnya, kita memiliki:

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

Kedua hasil tersebut mencirikan fungsi X → Filter X yang merupakan fungsi lingkungan bagi struktur ruang topologi pada X. Masih tersedia fungsi TopologicalSpace.mkOfNhds : (X → Filter X) → TopologicalSpace X, tetapi fungsi ini hanya akan mengembalikan masukannya sebagai fungsi lingkungan jika masukan tersebut memenuhi kedua syarat di atas. Lebih tepatnya, tersedia lema TopologicalSpace.nhds_mkOfNhds yang menyatakan hal ini dengan cara berbeda, dan latihan berikut akan menurunkan rumusan tersebut dari rumusan yang kita gunakan di atas.

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' := by
  sorry
end

Perhatikan bahwa TopologicalSpace.mkOfNhds tidak terlalu sering digunakan, tetapi tetap berguna untuk mengetahui dalam arti tepat apa filter-filter lingkungan memuat seluruh informasi dalam struktur ruang topologi.

Hal berikutnya yang perlu diketahui agar dapat menggunakan ruang topologi secara efisien di Mathlib ialah bahwa kita banyak memakai sifat formal TopologicalSpace : Type u → Type u. Dari sudut pandang matematika murni, sifat-sifat formal tersebut memberikan cara yang sangat bersih untuk menjelaskan bagaimana ruang topologi mengatasi masalah yang dimiliki ruang metrik. Dalam sudut pandang ini, masalah yang diatasi ialah bahwa ruang metrik hanya memiliki sedikit funktorialitas dan, secara umum, sifat kategorisnya sangat buruk. Hal ini melengkapi fakta yang telah dibahas bahwa ruang metrik memuat banyak informasi geometris yang tidak relevan secara topologis.

Mari kita berfokus terlebih dahulu pada funktorialitas. Struktur ruang metrik dapat diinduksi pada suatu himpunan bagian atau, secara ekuivalen, ditarik balik melalui pemetaan injektif. Namun, pada dasarnya hanya itu yang dapat dilakukan. Struktur tersebut tidak dapat ditarik balik melalui pemetaan umum ataupun didorong maju, bahkan melalui pemetaan surjektif.

Secara khusus, tidak ada jarak yang masuk akal untuk dipasang pada hasil bagi ruang metrik atau pada produk tak-terhitung dari ruang-ruang metrik. Sebagai contoh, pertimbangkan tipe ℝ → ℝ sebagai produk salinan ℝ yang diindeks oleh ℝ. Kita ingin mengatakan bahwa konvergensi titik demi titik pada barisan fungsi merupakan gagasan konvergensi yang layak. Namun, tidak ada jarak pada ℝ → ℝ yang menghasilkan gagasan konvergensi ini. Berkaitan dengan itu, tidak ada jarak yang menjamin bahwa pemetaan f : X → (ℝ → ℝ) kontinu jika dan hanya jika fun x ↦ f x t kontinu untuk setiap t : ℝ.

Sekarang kita tinjau data yang digunakan untuk mengatasi semua masalah tersebut. Pertama, kita dapat menggunakan sembarang pemetaan f : X → Y untuk mendorong atau menarik topologi dari satu sisi ke sisi lainnya. Kedua operasi ini membentuk koneksi Galois.

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

Operasi-operasi tersebut kompatibel dengan komposisi fungsi. Seperti biasa, pendorongan maju bersifat kovarian dan penarikan balik bersifat kontravarian; lihat coinduced_compose dan induced_compose. Di atas kertas, kita akan menggunakan notasi \(f_*T\) untuk TopologicalSpace.coinduced f T dan \(f^*T\) untuk TopologicalSpace.induced f T.

Bagian besar berikutnya adalah struktur kisi lengkap pada TopologicalSpace X untuk setiap X. Jika topologi terutama dipandang sebagai data himpunan terbuka, kita mengharapkan relasi urutan pada TopologicalSpace X berasal dari Set (Set X); yaitu, kita mengharapkan t ≤ t' jika himpunan u terbuka bagi t' setiap kali himpunan itu terbuka bagi t. Namun, kita sudah mengetahui bahwa Mathlib lebih berfokus pada lingkungan daripada himpunan terbuka. Karena itu, untuk setiap x : X, kita ingin pemetaan dari ruang topologi ke lingkungan fun T : TopologicalSpace X ↦ @nhds X T x mempertahankan urutan. Kita juga mengetahui bahwa relasi urutan pada Filter X dirancang agar principal : Set X → Filter X mempertahankan urutan, sehingga filter dapat dipandang sebagai himpunan tergeneralisasi. Jadi, relasi urutan yang digunakan pada TopologicalSpace X berlawanan dengan relasi yang berasal dari Set (Set X).

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

Sekarang kita dapat memperoleh kembali kekontinuan dengan menggabungkan operasi pendorongan maju (atau penarikan balik) dengan relasi urutan.

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

Dengan definisi ini dan kompatibilitas antara pendorongan maju dan komposisi, kita langsung memperoleh sifat universal berikut: untuk setiap ruang topologi \(Z\), fungsi \(g : Y → Z\) kontinu bagi topologi \(f_*T_X\) jika dan hanya jika \(g ∘ f\) kontinu.

\[\begin{split}g \text{ kontinu } &⇔ g_*(f_*T_X) ≤ T_Z \\ &⇔ (g ∘ f)_* T_X ≤ T_Z \\ &⇔ g ∘ f \text{ kontinu}\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]

Dengan demikian, kita sudah memperoleh topologi hasil bagi (dengan menggunakan pemetaan proyeksi sebagai f). Hasil ini belum menggunakan fakta bahwa TopologicalSpace X merupakan kisi lengkap bagi setiap X. Sekarang mari kita lihat bagaimana seluruh struktur ini membuktikan keberadaan topologi produk melalui abstraksi murni. Di atas kita mempertimbangkan kasus ℝ → ℝ; sekarang pertimbangkan kasus umum Π i, X i untuk suatu ι : Type* dan X : ι → Type*. Untuk setiap ruang topologis Z dan setiap fungsi f : Z → Π i, X i, kita ingin f kontinu jika dan hanya jika (fun x ↦ x i) ∘ f kontinu untuk semua i. Mari kita telusuri syarat tersebut “di atas kertas” dengan menggunakan notasi \(p_i\) untuk proyeksi (fun (x : Π i, X i) ↦ x i):

\[\begin{split}(∀ i, p_i ∘ f \text{ kontinu}) &⇔ ∀ i, (p_i ∘ f)_* T_Z ≤ T_{X_i} \\ &⇔ ∀ i, (p_i)_* f_* T_Z ≤ T_{X_i}\\ &⇔ ∀ i, f_* T_Z ≤ (p_i)^*T_{X_i}\\ &⇔ f_* T_Z ≤ \inf \left[(p_i)^*T_{X_i}\right]\end{split}\]

Jadi, kita dapat melihat topologi yang diinginkan pada Π 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

Dengan ini berakhirlah peninjauan kita tentang cara Mathlib memanfaatkan ruang topologis untuk mengatasi kekurangan teori ruang metrik: teorinya lebih funktorial dan memiliki struktur kisi lengkap untuk setiap tipe tetap.

11.3.2. Pemisahan dan keterhitungan

Kita telah melihat bahwa kategori ruang topologi memiliki sifat-sifat yang sangat baik. Harga yang harus dibayar adalah keberadaan ruang topologi yang cukup patologis. Ada sejumlah asumsi yang dapat dikenakan pada ruang topologi agar perilakunya lebih mendekati ruang metrik. Asumsi terpenting adalah T2Space, yang juga disebut “Hausdorff” dan menjamin bahwa limit bersifat unik. Sifat pemisahan yang lebih kuat adalah T3Space, yang selain itu menjamin sifat RegularSpace: setiap titik memiliki basis lingkungan tertutup.

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

Perhatikan bahwa, menurut definisi, setiap titik dalam setiap ruang topologi memiliki basis lingkungan terbuka.

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

Sasaran utama kita sekarang ialah membuktikan teorema dasar yang memungkinkan perluasan melalui kekontinuan. Dari buku topologi umum Bourbaki, I.8.5, Teorema 1 (dengan hanya mengambil implikasi nontrivial):

Misalkan \(X\) ruang topologi, \(A\) himpunan bagian padat dari \(X\), dan \(f : A → Y\) pemetaan kontinu dari \(A\) ke ruang \(T_3\) \(Y\). Jika, untuk setiap \(x\) dalam \(X\), nilai \(f(y)\) menuju suatu limit dalam \(Y\) ketika \(y\) menuju \(x\) sambil tetap berada dalam \(A\), maka terdapat perluasan kontinu \(φ\) dari \(f\) ke \(X\).

Sebenarnya, Mathlib memuat versi yang lebih umum dari lema di atas, yaitu IsDenseInducing.continuousAt_extend, tetapi di sini kita akan tetap memakai versi Bourbaki.

Ingat bahwa untuk A : Set X, ↥A adalah subtipe yang dikaitkan dengan A, dan Lean akan otomatis menyisipkan panah ke atas yang agak ganjil itu saat diperlukan. Pemetaan koersi (inklusi) adalah (↑) : A → X. Asumsi “menuju \(x\) sambil tetap berada dalam \(A\)” bersesuaian dengan filter penarikan balik comap (↑) (𝓝 x).

Pertama, mari kita buktikan sebuah lema bantu yang dipisahkan untuk menyederhanakan konteks (secara khusus, kita tidak memerlukan Y sebagai ruang topologis di sini).

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

Sekarang mari kita beralih ke bukti utama teorema perluasan melalui kekontinuan.

Ketika Lean memerlukan topologi pada ↥A, Lean akan otomatis menggunakan topologi terinduksi. Satu-satunya lema yang relevan adalah nhds_induced (↑) : ∀ a : ↥A, 𝓝 a = comap (↑) (𝓝 ↑a) (sebenarnya, ini adalah lema umum tentang topologi terinduksi).

Garis besar buktinya adalah sebagai berikut:

Asumsi utama dan aksioma pilihan memberikan fungsi φ sedemikian sehingga ∀ x, Tendsto f (comap (↑) (𝓝 x)) (𝓝 (φ x)) (karena Y bersifat Hausdorff, φ sepenuhnya ditentukan, tetapi kita belum memerlukan fakta itu sampai mencoba membuktikan bahwa φ memang memperluas f).

Pertama, mari kita buktikan bahwa φ kontinu. Tetapkan sembarang x : X. Karena Y reguler, cukup kita periksa bahwa untuk setiap lingkungan tertutup V' dari φ x, berlaku φ ⁻¹' V' ∈ 𝓝 x. Asumsi limit memberikan—melalui lema bantu di atas—suatu V ∈ 𝓝 x sedemikian sehingga IsOpen V ∧ (↑) ⁻¹' V ⊆ f ⁻¹' V'. Karena V ∈ 𝓝 x, cukup kita buktikan V ⊆ φ ⁻¹' V', yaitu ∀ y ∈ V, φ y ∈ V'. Tetapkan y dalam V. Karena V terbuka, himpunan ini merupakan lingkungan y. Secara khusus, (↑) ⁻¹' V ∈ comap (↑) (𝓝 y) dan, terlebih lagi, f ⁻¹' V' ∈ comap (↑) (𝓝 y). Selain itu, comap (↑) (𝓝 y) ≠ ⊥ karena A padat. Karena diketahui Tendsto f (comap (↑) (𝓝 y)) (𝓝 (φ y)), hal ini menyiratkan φ y ∈ closure V'. Karena V' tertutup, kita telah membuktikan φ y ∈ V'.

Tinggal membuktikan bahwa φ memperluas f. Pada tahap inilah kekontinuan f berperan, bersama dengan fakta bahwa Y bersifat Hausdorff.

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

Selain sifat pemisahan, jenis asumsi utama yang dapat dikenakan pada ruang topologis agar lebih mendekati ruang metrik adalah asumsi keterhitungan. Yang terpenting ialah keterhitungan pertama, yang mensyaratkan bahwa setiap titik memiliki basis lingkungan terhitung. Secara khusus, sifat ini memastikan bahwa penutupan himpunan dapat dipahami menggunakan barisan.

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

11.3.3. Kekompakan

Sekarang mari kita bahas cara kekompakan didefinisikan bagi ruang topologi. Seperti biasa, ada beberapa cara untuk memikirkannya, dan Mathlib memilih versi berbasis filter.

Pertama, kita perlu mendefinisikan titik gugus filter. Untuk filter F pada ruang topologi X, titik x : X merupakan titik gugus dari F jika F, yang dipandang sebagai himpunan tergeneralisasi, memiliki irisan tak-kosong dengan himpunan tergeneralisasi titik-titik yang dekat dengan x.

Selanjutnya, kita dapat mengatakan bahwa himpunan s kompak jika setiap himpunan tergeneralisasi tak-kosong F yang tercakup dalam s, yaitu yang memenuhi F ≤ 𝓟 s, memiliki titik gugus dalam 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

Sebagai contoh, jika F adalah map u atTop, yaitu citra melalui u : ℕ → X dari atTop—himpunan tergeneralisasi bilangan asli yang sangat besar—maka asumsi F ≤ 𝓟 s berarti bahwa u n termasuk dalam s untuk n yang cukup besar. Pernyataan bahwa x merupakan titik gugus dari map u atTop berarti bahwa citra bilangan-bilangan yang sangat besar beririsan dengan himpunan titik yang dekat dengan x. Jika 𝓝 x memiliki basis terhitung, kita dapat menafsirkannya sebagai pernyataan bahwa u memiliki subbarisan yang konvergen ke x; dengan demikian kita memperoleh kembali bentuk kekompakan dalam ruang metrik.

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

Titik gugus berperilaku baik terhadap fungsi kontinu.

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

Sebagai latihan, kita akan membuktikan bahwa citra himpunan kompak melalui pemetaan kontinu bersifat kompak. Selain hasil yang telah kita lihat, gunakan Filter.push_pull dan 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

Kekompakan juga dapat dinyatakan dalam kerangka selimut terbuka: s kompak jika setiap keluarga himpunan terbuka yang menyelimuti s memiliki subkeluarga berhingga yang tetap menyelimutinya.

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