.. _sets_and_functions:

Himpunan dan Fungsi
===================

Kosakata himpunan, relasi, dan fungsi menyediakan bahasa yang seragam
untuk melakukan konstruksi dalam semua cabang matematika.
Karena fungsi dan relasi dapat didefinisikan menggunakan himpunan,
teori himpunan aksiomatik dapat dipakai sebagai landasan matematika.

Sebaliknya, landasan Lean bertumpu pada gagasan primitif berupa *tipe*
dan mencakup cara-cara mendefinisikan fungsi di antara tipe.
Setiap ekspresi di Lean memiliki tipe:
ada bilangan asli, bilangan real, fungsi dari bilangan real ke bilangan real,
grup, ruang vektor, dan sebagainya.
Beberapa ekspresi *merupakan* tipe;
dengan kata lain,
tipenya adalah ``Type``.
Lean dan Mathlib menyediakan cara untuk mendefinisikan tipe baru
serta objek dari tipe-tipe tersebut.

Secara konseptual, tipe dapat dibayangkan sebagai suatu himpunan objek.
Persyaratan bahwa setiap objek memiliki tipe menawarkan beberapa keuntungan.
Sebagai contoh, persyaratan ini memungkinkan satu notasi seperti ``+`` dipakai
untuk berbagai operasi, dan terkadang membuat masukan lebih ringkas
karena Lean dapat menyimpulkan banyak informasi dari
tipe suatu objek.
Sistem tipe juga memungkinkan Lean menandai galat ketika Anda
menerapkan fungsi pada jumlah argumen yang keliru
atau pada argumen dengan tipe yang keliru.

Pustaka Lean tetap mendefinisikan gagasan-gagasan dasar teori himpunan.
Berbeda dengan teori himpunan,
di Lean suatu himpunan selalu merupakan himpunan objek dari tipe tertentu,
seperti himpunan bilangan asli atau himpunan fungsi
dari bilangan real ke bilangan real.
Perbedaan antara tipe dan himpunan perlu sedikit pembiasaan,
tetapi bab ini akan memandu Anda melalui pokok-pokok dasarnya.

.. include:: C04_Sets_and_Functions/S01_Sets.inc
.. include:: C04_Sets_and_Functions/S02_Functions.inc
.. include:: C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.inc