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

4.1. Himpunan

Jika α merupakan sembarang tipe, tipe Set α terdiri atas himpunan yang elemen-elemennya bertipe α. Tipe ini mendukung operasi dan relasi teori himpunan yang lazim. Sebagai contoh, s ⊆ t menyatakan bahwa s merupakan himpunan bagian dari t, s ∩ t menyatakan irisan s dan t, sedangkan s ∪ t menyatakan gabungannya. Relasi himpunan bagian dapat diketik dengan \ss atau \sub, irisan dengan \i atau \cap, dan gabungan dengan \un atau \cup. Pustaka juga mendefinisikan himpunan univ, yang terdiri atas semua elemen bertipe α, serta himpunan kosong, ∅, yang dapat diketik sebagai \empty. Untuk x : α dan s : Set α, ekspresi x ∈ s menyatakan bahwa x merupakan anggota s. Nama teorema yang menyebut keanggotaan himpunan sering kali memuat mem. Ekspresi x ∉ s menyingkat ¬ x ∈ s. Anda dapat mengetik ∈ sebagai \in atau \mem, dan ∉ sebagai \notin.

Salah satu cara membuktikan pernyataan tentang himpunan ialah memakai rw atau penyederhana untuk mengembangkan definisinya. Dalam contoh kedua di bawah, kita memakai simp only untuk meminta penyederhana hanya memakai daftar identitas yang kita berikan, bukan seluruh basis data identitasnya. Berbeda dengan rw, simp dapat melakukan penyederhanaan di dalam kuantor universal atau eksistensial. Jika Anda menelusuri bukti tersebut langkah demi langkah, Anda dapat melihat pengaruh perintah-perintah ini.

variable {α : Type*}
variable (s t u : Set α)
open Set

example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
  rw [subset_def, inter_def, inter_def]
  rw [subset_def] at h
  simp only [mem_setOf]
  rintro x ⟨xs, xu⟩
  exact ⟨h _ xs, xu⟩

example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
  simp only [subset_def, mem_inter_iff] at *
  rintro x ⟨xs, xu⟩
  exact ⟨h _ xs, xu⟩

Dalam contoh ini, kita membuka ruang nama Set agar dapat mengakses nama teorema yang lebih pendek. Namun, sebenarnya pemanggilan rw dan simp dapat dihapus seluruhnya:

example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
  intro x xsu
  exact ⟨h xsu.1, xsu.2⟩

Hal yang terjadi di sini dikenal sebagai reduksi definisional: agar dapat memahami perintah intro dan konstruktor anonim, Lean harus mengembangkan definisinya. Contoh berikut juga memperlihatkan fenomena tersebut:

example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u :=
  fun _x ⟨xs, xu⟩ ↦ ⟨h xs, xu⟩

Untuk menangani gabungan, kita dapat memakai Set.union_def dan Set.mem_union. Karena x ∈ s ∪ t terurai menjadi x ∈ s ∨ x ∈ t, kita juga dapat memakai taktik cases untuk memaksa reduksi definisional.

example : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
  intro x hx
  have xs : x ∈ s := hx.1
  have xtu : x ∈ t ∪ u := hx.2
  rcases xtu with xt | xu
  · left
    show x ∈ s ∩ t
    exact ⟨xs, xt⟩
  · right
    show x ∈ s ∩ u
    exact ⟨xs, xu⟩

Karena irisan mengikat lebih kuat daripada gabungan, tanda kurung dalam ekspresi (s ∩ t) ∪ (s ∩ u) sebenarnya tidak diperlukan, tetapi membuat maknanya lebih jelas. Berikut adalah bukti yang lebih pendek untuk fakta yang sama:

example : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
  rintro x ⟨xs, xt | xu⟩
  · left; exact ⟨xs, xt⟩
  · right; exact ⟨xs, xu⟩

Sebagai latihan, cobalah membuktikan inklusi yang sebaliknya:

example : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
  sorry

Perlu diketahui bahwa ketika memakai rintro, terkadang kita perlu mengapit pola disjungtif h1 | h2 dengan tanda kurung agar Lean menguraikannya dengan benar.

Pustaka juga mendefinisikan selisih himpunan, s \ t. Garis miring terbalik pada notasi tersebut merupakan karakter Unicode khusus yang dimasukkan sebagai \\. Ekspresi x ∈ s \ t terurai menjadi x ∈ s ∧ x ∉ t. (∉ dapat dimasukkan sebagai \notin.) Ekspresi ini dapat ditulis ulang secara manual memakai Set.diff_eq dan dsimp atau Set.mem_diff, tetapi dua bukti berikut untuk inklusi yang sama menunjukkan cara menghindari penggunaannya.

example : (s \ t) \ u ⊆ s \ (t ∪ u) := by
  intro x xstu
  have xs : x ∈ s := xstu.1.1
  have xnt : x ∉ t := xstu.1.2
  have xnu : x ∉ u := xstu.2
  constructor
  · exact xs
  intro xtu
  -- x ∈ t ∨ x ∈ u
  rcases xtu with xt | xu
  · show False; exact xnt xt
  · show False; exact xnu xu

example : (s \ t) \ u ⊆ s \ (t ∪ u) := by
  rintro x ⟨⟨xs, xnt⟩, xnu⟩
  use xs
  rintro (xt | xu) <;> contradiction

Sebagai latihan, buktikan inklusi yang sebaliknya:

example : s \ (t ∪ u) ⊆ (s \ t) \ u := by
  sorry

Untuk membuktikan bahwa dua himpunan sama, cukup ditunjukkan bahwa setiap elemen salah satunya juga merupakan elemen himpunan lainnya. Prinsip ini dikenal sebagai "ekstensionalitas" dan, sebagaimana dapat diduga, taktik ext dirancang untuk menanganinya.

example : s ∩ t = t ∩ s := by
  ext x
  simp only [mem_inter_iff]
  constructor
  · rintro ⟨xs, xt⟩; exact ⟨xt, xs⟩
  · rintro ⟨xt, xs⟩; exact ⟨xs, xt⟩

Sekali lagi, menghapus baris simp only [mem_inter_iff] tidak merusak bukti. Bahkan, jika Anda menyukai term bukti yang sukar dipahami, bukti satu baris berikut cocok untuk Anda:

example : s ∩ t = t ∩ s :=
  Set.ext fun _x ↦ ⟨fun ⟨xs, xt⟩ ↦ ⟨xt, xs⟩, fun ⟨xt, xs⟩ ↦ ⟨xs, xt⟩⟩

Berikut adalah bukti yang lebih pendek lagi, dengan memakai penyederhana:

example : s ∩ t = t ∩ s := by ext x; simp [and_comm]

Alternatif bagi penggunaan ext ialah memakai teorema Subset.antisymm, yang memungkinkan kita membuktikan persamaan s = t antara dua himpunan dengan membuktikan s ⊆ t dan t ⊆ s.

example : s ∩ t = t ∩ s := by
  apply Subset.antisymm
  · rintro x ⟨xs, xt⟩; exact ⟨xt, xs⟩
  · rintro x ⟨xt, xs⟩; exact ⟨xs, xt⟩

Cobalah melengkapi term bukti berikut:

example : s ∩ t = t ∩ s :=
    Subset.antisymm sorry sorry

Ingatlah bahwa Anda dapat mengganti sorry dengan garis bawah. Ketika penunjuk diarahkan ke garis bawah tersebut, Lean akan menunjukkan apa yang diharapkannya pada posisi itu.

Berikut beberapa identitas teori himpunan yang mungkin menarik untuk dibuktikan:

example : s ∩ (s ∪ t) = s := by
  sorry

example : s ∪ s ∩ t = s := by
  sorry

example : s \ t ∪ t = s ∪ t := by
  sorry

example : s \ t ∪ t \ s = (s ∪ t) \ (s ∩ t) := by
  sorry

Untuk memahami representasi himpunan, mari kita lihat cara kerjanya di balik layar. Dalam teori tipe, sebuah sifat atau predikat pada tipe α hanyalah fungsi P : α → Prop. Hal ini masuk akal: untuk a : α, P a hanyalah proposisi bahwa P berlaku pada a. Di dalam pustaka, Set α didefinisikan sebagai α → Prop, sedangkan x ∈ s didefinisikan sebagai s x. Dengan kata lain, himpunan sebenarnya merupakan sifat yang diperlakukan sebagai objek.

Pustaka juga mendefinisikan notasi pembentuk himpunan. Ekspresi { y | P y } terurai menjadi (fun y ↦ P y), sehingga x ∈ { y | P y } tereduksi menjadi P x. Jadi, sifat genap dapat kita ubah menjadi himpunan bilangan genap:

def evens : Set ℕ :=
  { n | Even n }

def odds : Set ℕ :=
  { n | ¬Even n }

example : evens ∪ odds = univ := by
  rw [evens, odds]
  ext n
  simp [-Nat.not_even_iff_odd]
  apply Classical.em

Telusurilah bukti ini langkah demi langkah dan pastikan Anda memahami apa yang terjadi. Perhatikan bahwa kita meminta penyederhana tidak memakai lema Nat.not_even_iff_odd karena kita ingin mempertahankan ¬ Even n di dalam sasaran. Cobalah menghapus baris rw [evens, odds] dan pastikan bahwa buktinya tetap berhasil.

Sebenarnya, notasi pembentuk himpunan dipakai untuk mendefinisikan

• s ∩ t sebagai {x | x ∈ s ∧ x ∈ t},

• s ∪ t sebagai {x | x ∈ s ∨ x ∈ t},

• ∅ sebagai {x | False}, dan

• univ sebagai {x | True}.

Kita sering perlu menyatakan tipe ∅ dan univ secara eksplisit, karena Lean kesulitan menebak tipe yang kita maksud. Contoh berikut menunjukkan cara Lean mengembangkan dua definisi terakhir ketika diperlukan. Dalam contoh kedua, trivial merupakan bukti kanonik bagi True di dalam pustaka.

example (x : ℕ) (h : x ∈ (∅ : Set ℕ)) : False :=
  h

example (x : ℕ) : x ∈ (univ : Set ℕ) :=
  trivial

Sebagai latihan, buktikan inklusi berikut. Gunakan intro n untuk mengembangkan definisi himpunan bagian, dan gunakan penyederhana untuk mereduksi konstruksi teori himpunan menjadi logika. Kami juga menyarankan penggunaan teorema Nat.Prime.eq_two_or_odd dan Nat.odd_iff.

example : { n | Nat.Prime n } ∩ { n | n > 2 } ⊆ { n | ¬Even n } := by
  sorry

Berhati-hatilah: pustaka memiliki beberapa versi predikat Prime, dan hal ini agak membingungkan. Versi yang paling umum bermakna pada sembarang monoid komutatif dengan elemen nol. Predikat Nat.Prime dikhususkan bagi bilangan asli. Untungnya, terdapat teorema yang menyatakan bahwa pada kasus khusus tersebut kedua gagasan ini berpadanan, sehingga salah satunya selalu dapat ditulis ulang menjadi yang lain.

#print Prime

#print Nat.Prime

example (n : ℕ) : Prime n ↔ Nat.Prime n :=
  Nat.prime_iff.symm

example (n : ℕ) (h : Prime n) : Nat.Prime n := by
  rw [Nat.prime_iff]
  exact h

Taktik rwa melakukan penulisan ulang, lalu mencoba menyelesaikan sasaran memakai asumsi yang tersedia.

example (n : ℕ) (h : Prime n) : Nat.Prime n := by
  rwa [Nat.prime_iff]

Lean memperkenalkan notasi ∀ x ∈ s, ..., "untuk setiap x di dalam s", sebagai singkatan bagi ∀ x, x ∈ s → .... Lean juga memperkenalkan notasi ∃ x ∈ s, ..., "terdapat x di dalam s sedemikian sehingga ...". Notasi-notasi ini terkadang disebut kuantor terbatas, karena konstruksinya membatasi jangkauan kuantor pada himpunan s. Akibatnya, nama teorema dalam pustaka yang memakainya sering kali memuat ball atau bex. Teorema bex_def menyatakan bahwa ∃ x ∈ s, ... ekuivalen dengan ∃ x, x ∈ s ∧ ..., tetapi ketika dipakai bersama rintro, use, dan konstruktor anonim, kedua ekspresi tersebut berperilaku kurang lebih sama. Karena itu, biasanya kita tidak perlu memakai bex_def untuk mentransformasikannya secara eksplisit. Berikut beberapa contoh penggunaannya:

variable (s t : Set ℕ)

example (h₀ : ∀ x ∈ s, ¬Even x) (h₁ : ∀ x ∈ s, Prime x) : ∀ x ∈ s, ¬Even x ∧ Prime x := by
  intro x xs
  constructor
  · apply h₀ x xs
  apply h₁ x xs

example (h : ∃ x ∈ s, ¬Even x ∧ Prime x) : ∃ x ∈ s, Prime x := by
  rcases h with ⟨x, xs, _, prime_x⟩
  use x, xs

Cobalah membuktikan beberapa variasi kecil berikut:

section
variable (ssubt : s ⊆ t)

example (h₀ : ∀ x ∈ t, ¬Even x) (h₁ : ∀ x ∈ t, Prime x) : ∀ x ∈ s, ¬Even x ∧ Prime x := by
  sorry

example (h : ∃ x ∈ s, ¬Even x ∧ Prime x) : ∃ x ∈ t, Prime x := by
  sorry

end

Gabungan dan irisan terindeks merupakan konstruksi teori himpunan penting lainnya. Kita dapat memodelkan barisan himpunan \(A_0, A_1, A_2, \ldots\) yang elemennya bertipe α sebagai fungsi A : ℕ → Set α. Dalam hal ini, ⋃ i, A i menyatakan gabungannya, sedangkan ⋂ i, A i menyatakan irisannya. Tidak ada yang istimewa dari bilangan asli di sini, sehingga ℕ dapat diganti dengan sembarang tipe I yang dipakai untuk mengindeks himpunan-himpunan tersebut. Contoh berikut memperlihatkan penggunaannya.

variable {α I : Type*}
variable (A B : I → Set α)
variable (s : Set α)

open Set

example : (s ∩ ⋃ i, A i) = ⋃ i, A i ∩ s := by
  ext x
  simp only [mem_inter_iff, mem_iUnion]
  constructor
  · rintro ⟨xs, ⟨i, xAi⟩⟩
    exact ⟨i, xAi, xs⟩
  rintro ⟨i, xAi, xs⟩
  exact ⟨xs, ⟨i, xAi⟩⟩

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ ⋂ i, B i := by
  ext x
  simp only [mem_inter_iff, mem_iInter]
  constructor
  · intro h
    constructor
    · intro i
      exact (h i).1
    intro i
    exact (h i).2
  rintro ⟨h1, h2⟩ i
  constructor
  · exact h1 i
  exact h2 i

Tanda kurung sering diperlukan pada gabungan atau irisan terindeks karena, seperti halnya pada kuantor, jangkauan variabel terikat meluas sejauh mungkin.

Cobalah membuktikan identitas berikut. Salah satu arahnya memerlukan logika klasik! Kami menyarankan penggunaan by_cases xs : x ∈ s pada tempat yang sesuai di dalam bukti.

example : (s ∪ ⋂ i, A i) = ⋂ i, A i ∪ s := by
  sorry

Mathlib juga memiliki gabungan dan irisan terbatas, yang analog dengan kuantor terbatas. Anda dapat mengurai maknanya dengan mem_iUnion₂ dan mem_iInter₂. Seperti diperlihatkan oleh contoh-contoh berikut, penyederhana Lean juga menjalankan penggantian tersebut.

def primes : Set ℕ :=
  { x | Nat.Prime x }

example : (⋃ p ∈ primes, { x | p ^ 2 ∣ x }) = { x | ∃ p ∈ primes, p ^ 2 ∣ x } := by
  ext
  rw [mem_iUnion₂]
  simp

example : (⋃ p ∈ primes, { x | p ^ 2 ∣ x }) = { x | ∃ p ∈ primes, p ^ 2 ∣ x } := by
  ext
  simp

example : (⋂ p ∈ primes, { x | ¬p ∣ x }) ⊆ { x | x = 1 } := by
  intro x
  contrapose!
  simp
  apply Nat.exists_prime_and_dvd

Cobalah menyelesaikan contoh serupa berikut. Jika Anda mulai mengetik eq_univ, pelengkapan tab akan menunjukkan bahwa apply eq_univ_of_forall merupakan cara yang baik untuk memulai bukti. Kami juga menyarankan penggunaan teorema Nat.exists_infinite_primes.

example : (⋃ p ∈ primes, { x | x ≤ p }) = univ := by
  sorry

Untuk suatu koleksi himpunan s : Set (Set α), gabungannya, ⋃₀ s, bertipe Set α dan didefinisikan sebagai {x | ∃ t ∈ s, x ∈ t}. Demikian pula, irisannya, ⋂₀ s, didefinisikan sebagai {x | ∀ t ∈ s, x ∈ t}. Kedua operasi ini masing-masing disebut sUnion dan sInter. Contoh berikut menunjukkan hubungannya dengan gabungan dan irisan terbatas.

variable {α : Type*} (s : Set (Set α))

example : ⋃₀ s = ⋃ t ∈ s, t := by
  ext x
  rw [mem_iUnion₂]
  simp

example : ⋂₀ s = ⋂ t ∈ s, t := by
  ext x
  rw [mem_iInter₂]
  rfl

Di dalam pustaka, identitas-identitas ini disebut sUnion_eq_biUnion dan sInter_eq_biInter.

4.2. Fungsi

Jika f : α → β adalah sebuah fungsi dan p adalah himpunan yang beranggotakan elemen bertipe β, pustaka mendefinisikan preimage f p, yang ditulis f ⁻¹' p, sebagai {x | f x ∈ p}. Ekspresi x ∈ f ⁻¹' p tereduksi menjadi f x ∈ p. Hal ini sering kali memudahkan, seperti pada contoh berikut:

variable {α β : Type*}
variable (f : α → β)
variable (s t : Set α)
variable (u v : Set β)

open Function
open Set

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by
  ext
  rfl

Jika s adalah himpunan yang beranggotakan elemen bertipe α, pustaka juga mendefinisikan image f s, yang ditulis f '' s, sebagai {y | ∃ x, x ∈ s ∧ f x = y}. Dengan demikian, hipotesis y ∈ f '' s dapat diuraikan menjadi tripel ⟨x, xs, xeq⟩ dengan x : α yang memenuhi hipotesis xs : x ∈ s dan xeq : f x = y. Tag rfl dalam taktik rintro (lihat Bab 3.2) dibuat khusus untuk situasi semacam ini.

example : f '' (s ∪ t) = f '' s ∪ f '' t := by
  ext y; constructor
  · rintro ⟨x, xs | xt, rfl⟩
    · left
      use x, xs
    right
    use x, xt
  rintro (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩)
  · use x, Or.inl xs
  use x, Or.inr xt

Perhatikan pula bahwa taktik use menerapkan rfl untuk menutup sasaran jika memungkinkan.

Berikut contoh lain:

example : s ⊆ f ⁻¹' (f '' s) := by
  intro x xs
  show f x ∈ f '' s
  use x, xs

Kita dapat mengganti baris use x, xs dengan apply mem_image_of_mem f xs jika ingin memakai teorema yang dirancang khusus untuk tujuan tersebut. Namun, mengetahui bahwa citra didefinisikan melalui kuantor eksistensial sering kali berguna.

Kesetaraan berikut merupakan latihan yang baik:

example : f '' s ⊆ v ↔ s ⊆ f ⁻¹' v := by
  sorry

Ini menunjukkan bahwa image f dan preimage f merupakan contoh dari apa yang dikenal sebagai koneksi Galois antara Set α dan Set β, yang masing-masing terurut parsial oleh relasi himpunan bagian. Di pustaka, kesetaraan ini bernama image_subset_iff. Dalam praktik, ruas kanan sering kali merupakan representasi yang lebih berguna, karena x ∈ f ⁻¹' t terurai menjadi f x ∈ t, sedangkan bekerja dengan y ∈ f '' s mengharuskan kita menguraikan sebuah kuantor eksistensial.

Berikut daftar panjang identitas teori himpunan untuk Anda nikmati. Anda tidak perlu mengerjakan semuanya sekaligus; kerjakan beberapa di antaranya, lalu simpan sisanya untuk kesempatan lain.

example (h : Injective f) : f ⁻¹' (f '' s) ⊆ s := by
  sorry

example : f '' (f ⁻¹' u) ⊆ u := by
  sorry

example (h : Surjective f) : u ⊆ f '' (f ⁻¹' u) := by
  sorry

example (h : s ⊆ t) : f '' s ⊆ f '' t := by
  sorry

example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by
  sorry

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v := by
  sorry

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by
  sorry

example (h : Injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := by
  sorry

example : f '' s \ f '' t ⊆ f '' (s \ t) := by
  sorry

example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) := by
  sorry

example : f '' s ∩ v = f '' (s ∩ f ⁻¹' v) := by
  sorry

example : f '' (s ∩ f ⁻¹' u) ⊆ f '' s ∩ u := by
  sorry

example : s ∩ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∩ u) := by
  sorry

example : s ∪ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∪ u) := by
  sorry

Anda juga dapat mencoba rangkaian latihan berikut, yang mencirikan perilaku citra dan prapeta terhadap gabungan dan irisan terindeks. Dalam latihan ketiga, argumen i : I diperlukan untuk menjamin bahwa himpunan indeks tidak kosong. Untuk membuktikan latihan-latihan ini, kami menyarankan penggunaan ext atau intro untuk menguraikan makna persamaan atau inklusi antarhimpunan, lalu memanggil simp untuk menguraikan syarat keanggotaan.

variable {I : Type*} (A : I → Set α) (B : I → Set β)

example : (f '' ⋃ i, A i) = ⋃ i, f '' A i := by
  sorry

example : (f '' ⋂ i, A i) ⊆ ⋂ i, f '' A i := by
  sorry

example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i := by
  sorry

example : (f ⁻¹' ⋃ i, B i) = ⋃ i, f ⁻¹' B i := by
  sorry

example : (f ⁻¹' ⋂ i, B i) = ⋂ i, f ⁻¹' B i := by
  sorry

Pustaka mendefinisikan predikat InjOn f s untuk menyatakan bahwa f injektif pada s. Definisinya adalah sebagai berikut:

example : InjOn f s ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ s, f x₁ = f x₂ → x₁ = x₂ :=
  Iff.refl _

Pernyataan Injective f terbukti ekuivalen dengan InjOn f univ. Demikian pula, pustaka mendefinisikan range f sebagai {x | ∃y, f y = x}, sehingga range f terbukti sama dengan f '' univ. Ini merupakan tema yang umum di Mathlib: meskipun banyak sifat fungsi didefinisikan pada seluruh domainnya, sering tersedia versi relatif yang membatasi pernyataan tersebut pada suatu himpunan bagian dari tipe domain.

Berikut beberapa contoh penggunaan InjOn dan range:

open Set Real

example : InjOn log { x | x > 0 } := by
  intro x xpos y ypos e
  calc
    x = exp (log x) := by rw [exp_log xpos]
    _ = exp (log y) := by rw [e]
    _ = y := by rw [exp_log ypos]


example : range exp = { y | y > 0 } := by
  ext y; constructor
  · rintro ⟨x, rfl⟩
    apply exp_pos
  intro ypos
  use log y
  rw [exp_log ypos]

Cobalah buktikan pernyataan-pernyataan berikut:

example : InjOn sqrt { x | x ≥ 0 } := by
  sorry

example : InjOn (fun x ↦ x ^ 2) { x : ℝ | x ≥ 0 } := by
  sorry

example : sqrt '' { x | x ≥ 0 } = { y | y ≥ 0 } := by
  sorry

example : (range fun x ↦ x ^ 2) = { y : ℝ | y ≥ 0 } := by
  sorry

Untuk mendefinisikan invers dari fungsi f : α → β, kita akan memakai dua unsur baru. Pertama, kita perlu menghadapi kenyataan bahwa sembarang tipe di Lean mungkin saja kosong. Untuk mendefinisikan invers f pada y ketika tidak ada x yang memenuhi f x = y, kita ingin menetapkan nilai bawaan di α. Menambahkan anotasi [Inhabited α] sebagai variabel setara dengan mengasumsikan bahwa α memiliki elemen pilihan, yang dinyatakan dengan default. Kedua, jika terdapat lebih dari satu x yang memenuhi f x = y, fungsi invers perlu memilih salah satunya. Hal ini memerlukan aksioma pilihan. Lean menyediakan berbagai cara untuk mengaksesnya; salah satu cara yang praktis ialah menggunakan operator klasik choose, seperti diperlihatkan di bawah ini.

variable {α β : Type*} [Inhabited α]

#check (default : α)

variable (P : α → Prop) (h : ∃ x, P x)

#check Classical.choose h

example : P (Classical.choose h) :=
  Classical.choose_spec h

Diberikan h : ∃ x, P x, nilai Classical.choose h adalah suatu x yang memenuhi P x. Teorema Classical.choose_spec h menyatakan bahwa Classical.choose h memenuhi spesifikasi ini.

Dengan kedua unsur tersebut, kita dapat mendefinisikan fungsi invers sebagai berikut:

noncomputable section

open Classical

def inverse (f : α → β) : β → α := fun y : β ↦
  if h : ∃ x, f x = y then Classical.choose h else default

theorem inverse_spec {f : α → β} (y : β) (h : ∃ x, f x = y) : f (inverse f y) = y := by
  rw [inverse, dif_pos h]
  exact Classical.choose_spec h

Baris noncomputable section dan open Classical diperlukan karena kita menggunakan logika klasik secara esensial. Untuk masukan y, fungsi inverse f mengembalikan suatu nilai x yang memenuhi f x = y jika nilai itu ada, dan mengembalikan elemen bawaan dari α jika tidak. Ini merupakan contoh konstruksi if dependen, karena dalam kasus positif, nilai yang dikembalikan, Classical.choose h, bergantung pada asumsi h. Identitas dif_pos h menulis ulang if h : e then a else b menjadi a jika diberikan h : e, dan, serupa dengan itu, dif_neg h menulis ulang ekspresi tersebut menjadi b jika diberikan h : ¬ e. Tersedia pula versi if_pos dan if_neg yang berlaku untuk konstruksi if nondependen dan akan digunakan dalam bagian berikutnya. Teorema inverse_spec menyatakan bahwa inverse f memenuhi bagian pertama spesifikasi ini.

Jangan khawatir jika Anda belum sepenuhnya memahami cara kerja semua ini. Teorema inverse_spec saja semestinya cukup untuk menunjukkan bahwa inverse f merupakan invers kiri jika dan hanya jika f injektif, serta merupakan invers kanan jika dan hanya jika f surjektif. Carilah definisi LeftInverse dan RightInverse dengan mengeklik ganda atau mengeklik kanan keduanya di VS Code, atau dengan menggunakan perintah #print LeftInverse dan #print RightInverse. Kemudian cobalah buktikan kedua teorema tersebut. Keduanya cukup rumit! Sebaiknya kerjakan dahulu buktinya di atas kertas sebelum Anda mulai mengutak-atik rinciannya. Anda seharusnya dapat membuktikan masing-masing teorema dengan sekitar enam baris pendek. Jika menginginkan tantangan tambahan, cobalah padatkan setiap bukti menjadi term bukti satu baris.

variable (f : α → β)

open Function

example : Injective f ↔ LeftInverse (inverse f) f :=
  sorry

example : Surjective f ↔ RightInverse (inverse f) f :=
  sorry

Kita menutup bagian ini dengan versi dalam teori tipe dari teorema Cantor yang terkenal: tidak ada fungsi surjektif dari suatu himpunan ke himpunan kuasanya. Cobalah pahami buktinya, lalu lengkapi dua baris yang masih kosong.

theorem Cantor : ∀ f : α → Set α, ¬Surjective f := by
  intro f surjf
  let S := { i | i ∉ f i }
  rcases surjf S with ⟨j, h⟩
  have h₁ : j ∉ f j := by
    intro h'
    have : j ∉ f j := by rwa [h] at h'
    contradiction
  have h₂ : j ∈ S
  sorry
  have h₃ : j ∉ S
  sorry
  contradiction

4.3. Teorema Schröder–Bernstein

Kita menutup bab ini dengan sebuah teorema teori himpunan yang elementer tetapi tidak sepele. Misalkan \(\alpha\) dan \(\beta\) adalah himpunan. (Dalam formalisasi kita, keduanya sebenarnya berupa tipe.) Andaikan \(f : \alpha → \beta\) dan \(g : \beta → \alpha\) keduanya injektif. Secara intuitif, ini berarti bahwa \(\alpha\) tidak lebih besar daripada \(\beta\), dan sebaliknya. Jika \(\alpha\) dan \(\beta\) berhingga, hal ini menyiratkan bahwa keduanya memiliki kardinalitas yang sama, yang ekuivalen dengan adanya bijeksi di antara keduanya. Pada abad kesembilan belas, Cantor menyatakan bahwa hasil yang sama tetap berlaku ketika \(\alpha\) dan \(\beta\) tak berhingga. Hal ini akhirnya dibuktikan secara terpisah oleh Dedekind, Schröder, dan Bernstein.

Formalisasi kita akan memperkenalkan beberapa metode baru yang akan dijelaskan secara lebih terperinci dalam bab-bab mendatang. Jangan khawatir jika pembahasannya terasa terlalu cepat di sini. Tujuan kami adalah menunjukkan bahwa Anda sudah memiliki keterampilan untuk berkontribusi pada pembuktian formal sebuah hasil matematika yang nyata.

Untuk memahami gagasan di balik bukti ini, perhatikan citra pemetaan \(g\) di \(\alpha\). Pada citra tersebut, invers \(g\) terdefinisi dan merupakan bijeksi dengan \(\beta\).

Masalahnya, bijeksi tersebut tidak mencakup daerah berarsir pada diagram, yang tidak kosong jika \(g\) tidak surjektif. Sebagai alternatif, kita dapat menggunakan \(f\) untuk memetakan seluruh \(\alpha\) ke \(\beta\), tetapi jika \(f\) tidak surjektif, pemetaan itu akan melewatkan beberapa elemen \(\beta\).

Sekarang perhatikan komposisi \(g \circ f\) dari \(\alpha\) ke dirinya sendiri. Karena komposisi ini injektif, ia membentuk bijeksi antara \(\alpha\) dan citranya, sehingga menghasilkan salinan \(\alpha\) berskala lebih kecil di dalam dirinya sendiri.

Komposisi ini memetakan cincin berarsir bagian dalam ke himpunan lain yang serupa, yang dapat kita bayangkan sebagai cincin berarsir konsentris yang lebih kecil lagi, dan demikian seterusnya. Dengan cara ini diperoleh barisan konsentris cincin berarsir, yang masing-masing berkorespondensi secara bijektif dengan cincin berikutnya. Jika kita memetakan setiap cincin ke cincin berikutnya dan membiarkan bagian \(\alpha\) yang tidak berarsir tetap di tempatnya, kita memperoleh bijeksi antara \(\alpha\) dan citra \(g\). Dengan mengomposisikannya dengan \(g^{-1}\), kita memperoleh bijeksi yang diinginkan antara \(\alpha\) dan \(\beta\).

Kita dapat mendeskripsikan bijeksi ini secara lebih sederhana. Misalkan \(A\) adalah gabungan barisan daerah berarsir tersebut, dan definisikan \(h : \alpha \to \beta\) sebagai berikut:

\[\begin{split}h(x) = \begin{cases} f(x) & \text{jika $x \in A$} \\ g^{-1}(x) & \text{jika tidak.} \end{cases}\end{split}\]

Dengan kata lain, kita menggunakan \(f\) pada bagian yang berarsir, dan menggunakan invers \(g\) di tempat lain. Pemetaan \(h\) yang dihasilkan bersifat injektif karena setiap komponennya injektif dan citra kedua komponen tersebut saling lepas. Untuk melihat bahwa pemetaan ini surjektif, misalkan diberikan \(y\) di \(\beta\), lalu perhatikan \(g(y)\). Jika \(g(y)\) berada di salah satu daerah berarsir, ia tidak mungkin berada di cincin pertama, sehingga \(g(y) = g(f(x))\) untuk suatu \(x\) yang berada di cincin sebelumnya. Dari injektivitas \(g\), kita memperoleh \(h(x) = f(x) = y\). Jika \(g(y)\) tidak berada di daerah berarsir, maka menurut definisi \(h\), kita memiliki \(h(g(y)) = y\). Dalam kedua kasus, \(y\) berada di dalam citra \(h\).

Argumen ini terdengar masuk akal, tetapi rinciannya cukup pelik. Memformalkan bukti tersebut tidak hanya meningkatkan keyakinan kita terhadap hasilnya, tetapi juga membantu kita memahaminya dengan lebih baik. Karena bukti ini menggunakan logika klasik, kita memberi tahu Lean bahwa definisi kita secara umum tidak dapat dikomputasi.

noncomputable section
open Classical
variable {α β : Type*} [Nonempty β]

Anotasi [Nonempty β] menyatakan bahwa β tidak kosong. Kita memakainya karena primitif Mathlib yang akan digunakan untuk membangun \(g^{-1}\) memerlukan anotasi tersebut. Kasus teorema ketika \(\beta\) kosong bersifat trivial, dan meskipun formalisasi ini tidak sulit digeneralisasi agar mencakup kasus itu juga, kita tidak akan melakukannya di sini. Secara khusus, kita memerlukan hipotesis [Nonempty β] untuk operasi invFun yang didefinisikan di Mathlib. Diberikan x : α, invFun g x memilih prapeta dari x di β jika ada, dan mengembalikan sembarang elemen β jika tidak ada. Fungsi invFun g selalu merupakan invers kiri jika g injektif dan invers kanan jika g surjektif.

#check (invFun g : α → β)
#check (leftInverse_invFun : Injective g → LeftInverse (invFun g) g)
#check (leftInverse_invFun : Injective g → ∀ y, invFun g (g y) = y)
#check (invFun_eq : (∃ y, g y = x) → g (invFun g x) = x)

Kita mendefinisikan himpunan yang berkorespondensi dengan gabungan daerah berarsir sebagai berikut.

variable (f : α → β) (g : β → α)

def sbAux : ℕ → Set α
  | 0 => univ \ g '' univ
  | n + 1 => g '' (f '' sbAux n)

def sbSet :=
  ⋃ n, sbAux f g n

Definisi sbAux merupakan contoh definisi rekursif, yang akan kita jelaskan dalam bab berikutnya. Definisi ini menghasilkan barisan himpunan

\[\begin{split}S_0 &= \alpha ∖ g(\beta) \\ S_{n+1} &= g(f(S_n)).\end{split}\]

Definisi sbSet berkorespondensi dengan himpunan \(A = \bigcup_{n \in \mathbb{N}} S_n\) dalam sketsa bukti kita. Fungsi \(h\) yang dijelaskan di atas kini didefinisikan sebagai berikut:

def sbFun (x : α) : β :=
  if x ∈ sbSet f g then f x else invFun g x

Kita akan memerlukan fakta bahwa definisi kita untuk \(g^{-1}\) merupakan invers kanan pada komplemen \(A\), yakni pada daerah \(\alpha\) yang tidak berarsir. Hal ini berlaku karena cincin terluar, \(S_0\), sama dengan \(\alpha \setminus g(\beta)\), sehingga komplemen \(A\) termuat di dalam \(g(\beta)\). Akibatnya, untuk setiap \(x\) di komplemen \(A\), terdapat \(y\) sedemikian sehingga \(g(y) = x\). (Menurut injektivitas \(g\), \(y\) ini tunggal, tetapi teorema berikut hanya menyatakan bahwa invFun g x mengembalikan suatu y sedemikian sehingga g y = x.)

Telusurilah bukti di bawah ini, pastikan Anda memahami apa yang terjadi, lalu lengkapi bagian-bagian yang tersisa. Anda perlu menggunakan invFun_eq di bagian akhir. Perhatikan bahwa penulisan ulang dengan sbAux di sini mengganti sbAux f g 0 dengan ruas kanan persamaan definisi yang bersesuaian.

theorem sb_right_inv {x : α} (hx : x ∉ sbSet f g) : g (invFun g x) = x := by
  have : x ∈ g '' univ := by
    contrapose! hx
    rw [sbSet, mem_iUnion]
    use 0
    rw [sbAux, mem_diff]
    sorry
  have : ∃ y, g y = x := by
    sorry
  sorry

Sekarang kita beralih ke pembuktian bahwa \(h\) injektif. Secara informal, buktinya berjalan sebagai berikut. Pertama, misalkan \(h(x_1) = h(x_2)\). Jika \(x_1\) berada di \(A\), maka \(h(x_1) = f(x_1)\), dan kita dapat menunjukkan bahwa \(x_2\) berada di \(A\) sebagai berikut. Jika tidak, maka \(h(x_2) = g^{-1}(x_2)\). Dari \(f(x_1) = h(x_1) = h(x_2)\) diperoleh \(g(f(x_1)) = x_2\). Menurut definisi \(A\), karena \(x_1\) berada di \(A\), \(x_2\) juga berada di \(A\), suatu kontradiksi. Jadi, jika \(x_1\) berada di \(A\), demikian pula \(x_2\), sehingga \(f(x_1) = h(x_1) = h(x_2) = f(x_2)\). Injektivitas \(f\) kemudian menyiratkan \(x_1 = x_2\). Argumen simetris menunjukkan bahwa jika \(x_2\) berada di \(A\), maka \(x_1\) juga berada di sana, yang kembali menyiratkan \(x_1 = x_2\).

Satu-satunya kemungkinan yang tersisa ialah baik \(x_1\) maupun \(x_2\) tidak berada di \(A\). Dalam kasus ini, \(g^{-1}(x_1) = h(x_1) = h(x_2) = g^{-1}(x_2)\). Menerapkan \(g\) pada kedua ruas menghasilkan \(x_1 = x_2\).

Sekali lagi, kami menganjurkan Anda menelusuri bukti berikut untuk melihat bagaimana argumen ini berlangsung di Lean. Cobalah menyelesaikan bukti tersebut dengan menggunakan sb_right_inv.

theorem sb_injective (hf : Injective f) : Injective (sbFun f g) := by
  set A := sbSet f g with A_def
  set h := sbFun f g with h_def
  intro x₁ x₂ (hxeq : h x₁ = h x₂)
  show x₁ = x₂
  simp only [h_def, sbFun, ← A_def] at hxeq
  by_cases xA : x₁ ∈ A ∨ x₂ ∈ A
  · wlog x₁A : x₁ ∈ A generalizing x₁ x₂ hxeq xA
    · symm
      apply this hxeq.symm xA.symm (xA.resolve_left x₁A)
    have x₂A : x₂ ∈ A := by
      apply _root_.not_imp_self.mp
      intro (x₂nA : x₂ ∉ A)
      rw [if_pos x₁A, if_neg x₂nA] at hxeq
      rw [A_def, sbSet, mem_iUnion] at x₁A
      have x₂eq : x₂ = g (f x₁) := by
        sorry
      rcases x₁A with ⟨n, hn⟩
      rw [A_def, sbSet, mem_iUnion]
      use n + 1
      simp [sbAux]
      exact ⟨x₁, hn, x₂eq.symm⟩
    sorry
  push_neg at xA
  sorry

Bukti ini memperkenalkan beberapa taktik baru. Pertama-tama, perhatikan taktik set, yang memperkenalkan singkatan A dan h masing-masing untuk sbSet f g dan sbFun f g. Kita menamai persamaan definisi yang bersesuaian A_def dan h_def. Singkatan tersebut bersifat definisional; artinya, Lean kadang-kadang menguraikannya secara otomatis ketika diperlukan. Namun tidak selalu; misalnya, ketika menggunakan rw, biasanya kita perlu menggunakan A_def dan h_def secara eksplisit. Jadi, ada kompromi dalam menggunakan definisi ini: ekspresi dapat menjadi lebih ringkas dan lebih mudah dibaca, tetapi kadang-kadang kita perlu melakukan lebih banyak pekerjaan.

Taktik yang lebih menarik adalah wlog, yang merangkum argumen simetri dalam bukti informal di atas. Kita tidak akan membahasnya panjang lebar sekarang, tetapi perhatikan bahwa taktik ini bekerja tepat seperti yang kita perlukan. Anda dapat mengarahkan kursor ke taktik tersebut untuk melihat dokumentasinya.

Argumen untuk surjektivitas bahkan lebih mudah. Diberikan \(y\) di \(\beta\), kita mempertimbangkan dua kasus, bergantung pada apakah \(g(y)\) berada di \(A\). Jika ya, ia tidak mungkin berada di \(S_0\), cincin terluar, karena menurut definisi cincin tersebut terpisah dari citra \(g\). Jadi, ia merupakan elemen \(S_{n+1}\) untuk suatu \(n\). Artinya, ia berbentuk \(g(f(x))\) untuk suatu \(x\) di \(S_n\). Dari injektivitas \(g\), kita memperoleh \(f(x) = y\). Jika \(g(y)\) berada di komplemen \(A\), kita langsung memiliki \(h(g(y)) = y\), dan bukti selesai.

Sekali lagi, kami menganjurkan Anda menelusuri bukti tersebut dan melengkapi bagian-bagian yang kosong. Taktik rcases n with _ | n membagi pembuktian menjadi kasus g y ∈ sbAux f g 0 dan g y ∈ sbAux f g (n + 1). Dalam kedua kasus, memanggil penyederhana dengan simp [sbAux] menerapkan persamaan definisi sbAux yang bersesuaian.

theorem sb_surjective (hg : Injective g) : Surjective (sbFun f g) := by
  set A := sbSet f g with A_def
  set h := sbFun f g with h_def
  intro y
  by_cases gyA : g y ∈ A
  · rw [A_def, sbSet, mem_iUnion] at gyA
    rcases gyA with ⟨n, hn⟩
    rcases n with _ | n
    · simp [sbAux] at hn
    simp [sbAux] at hn
    rcases hn with ⟨x, xmem, hx⟩
    use x
    have : x ∈ A := by
      rw [A_def, sbSet, mem_iUnion]
      exact ⟨n, xmem⟩
    rw [h_def, sbFun, if_pos this]
    apply hg hx

  sorry

Sekarang kita dapat menyatukan semuanya. Pernyataan akhirnya ringkas, dan buktinya menggunakan fakta bahwa Bijective h terurai menjadi Injective h ∧ Surjective h.

theorem schroeder_bernstein {f : α → β} {g : β → α} (hf : Injective f) (hg : Injective g) :
    ∃ h : α → β, Bijective h :=
  ⟨sbFun f g, sb_injective f g hf, sb_surjective f g hg⟩