.. _topology:

.. index:: topologi

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 :math:`f(x)` adalah nilai :math:`b`
ketika :math:`x` mendekati nilai :math:`a`,
atau bahwa :math:`f(x)` *konvergen ke* :math:`b` ketika :math:`x` mendekati :math:`a`.
Secara ekuivalen, kita dapat mengatakan bahwa :math:`f(x)` mendekati :math:`b`
ketika :math:`x` mendekati nilai :math:`a`, atau bahwa fungsi itu *menuju* :math:`b`
ketika :math:`x` menuju :math:`a`.
Kita telah mulai membahas gagasan-gagasan semacam ini dalam
:numref:`sequences_and_convergence`.

*Topologi* adalah kajian abstrak tentang limit dan kekontinuan.
Setelah membahas pokok-pokok formalisasi dalam Bab :numref:`%s <basics>`
hingga :numref:`%s <structures>`,
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 :numref:`Bab %s <sets_and_functions>`.
Lapisan berikutnya adalah teori *filter*, yang akan kita uraikan dalam
:numref:`filters`.
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 :numref:`sequences_and_convergence`.

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.

.. include:: C11_Topology/S01_Filters.inc
.. include:: C11_Topology/S02_Metric_Spaces.inc
.. include:: C11_Topology/S03_Topological_Spaces.inc