Аналіз I, Глава 3.3

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Поняття функції Function X Y між двома множинами X, Y в теорії множин із глави 3.1
• Різні співвідношення з поняттям функції X → Y у Mathlib між двома типами X, Y. (Примітка із глави 3.1, що кожна Set X також може бути розглянути як підтип { x:Object // x ∈ X } Object.)
• Basic function properties and operations, such as composition, one-to-one and onto functions, and inverses. Основні властивості та операції над функціями, такі як композиція, ін'єктивні функції, сур'єктивні функції, та обернені функції.

У решті книги ми відмовимося від версії функції із Розділу 3 та працюватимемо з поняттям функції із Mathlib. Навіть у цьому розділі ми перейдемо до формалізму Mathlib для деяких прикладів, що стосуються систем числення, таких як ℤ або ℝ, які не були реалізовані у фреймворку Розділу 3.

structure Chapter3.Function [SetTheory] (X Y : Set) : Type

Визначення 3.3.1. Function X Y — це структура функцій із X до Y. Аналогічно типу Mathlib X → Y.

• P : X.toSubtype → Y.toSubtype → Prop
• unique (x : X.toSubtype) : ∃! y : Y.toSubtype, self.P x y

theorem Chapter3.Function.ext {inst✝ : SetTheory} {X Y : Set} {x y : Function X Y} (P : x.P = y.P) : x = y

theorem Chapter3.Function.ext_iff {inst✝ : SetTheory} {X Y : Set} {x y : Function X Y} : x = y ↔ x.P = y.P

noncomputable instance Chapter3.Function.inst_coefn [SetTheory] (X Y : Set) : CoeFun (Function X Y) fun (x : Function X Y) => X.toSubtype → Y.toSubtype

Перетворення функції f: Function X Y із Розділу 3 на функцію Mathlib f: X → Y. Визначення функції із Розділу 3 було неконструктивним, тому тут нам доведеться використати аксіому вибору.

Equations

• Chapter3.Function.inst_coefn X Y = { coe := fun (f : Chapter3.Function X Y) (x : X.toSubtype) => Classical.choose ⋯ }

@[reducible, inline]

noncomputable abbrev Chapter3.Function.to_fn [SetTheory] {X Y : Set} (f : Function X Y) (x : X.toSubtype) : Y.toSubtype

Equations

• f.to_fn x = (fun (x : X.toSubtype) => Classical.choose ⋯) x

theorem Chapter3.Function.to_fn_eval [SetTheory] {X Y : Set} (f : Function X Y) (x : X.toSubtype) : f.to_fn x = (fun (x : X.toSubtype) => Classical.choose ⋯) x

@[reducible, inline]

abbrev Chapter3.Function.mk_fn [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) : Function X Y

Перетворення функції Mathlib на функцію з Розділу 3

Equations

• Chapter3.Function.mk_fn f = { P := fun (x : X.toSubtype) (y : Y.toSubtype) => y = f x, unique := ⋯ }

theorem Chapter3.Function.eval [SetTheory] {X Y : Set} (f : Function X Y) (x : X.toSubtype) (y : Y.toSubtype) : y = (fun (x : X.toSubtype) => Classical.choose ⋯) x ↔ f.P x y

Визначення 3.3.1

@[simp]

theorem Chapter3.Function.eval_of [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (x : X.toSubtype) : (fun (x : X.toSubtype) => Classical.choose ⋯) x = f x

@[reducible, inline]

abbrev Chapter3.P_3_3_2a [SetTheory] : nat.toSubtype → nat.toSubtype → Prop

Приклад 3.3.2.

Equations

• Chapter3.P_3_3_2a x y = (Chapter3.SetTheory.Set.nat_equiv.symm y = Chapter3.SetTheory.Set.nat_equiv.symm x + 1)

theorem Chapter3.SetTheory.Set.P_3_3_2a_existsUnique [SetTheory] (x : nat.toSubtype) : ∃! y : nat.toSubtype, P_3_3_2a x y

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_2a [SetTheory] : Function nat nat

Equations

• Chapter3.SetTheory.Set.f_3_3_2a = { P := Chapter3.P_3_3_2a, unique := ⋯ }

theorem Chapter3.SetTheory.Set.f_3_3_2a_eval [SetTheory] (x y : nat.toSubtype) : y = (fun (x : nat.toSubtype) => Classical.choose ⋯) x ↔ nat_equiv.symm y = nat_equiv.symm x + 1

theorem Chapter3.SetTheory.Set.f_3_3_2a_eval' [SetTheory] (n : ℕ) : (fun (x : nat.toSubtype) => Classical.choose ⋯) ↑n = ↑(n + 1)

theorem Chapter3.SetTheory.Set.f_3_3_2a_eval'' [SetTheory] : (fun (x : nat.toSubtype) => Classical.choose ⋯) 4 = 5

theorem Chapter3.SetTheory.Set.f_3_3_2a_eval''' [SetTheory] (n : ℕ) : (fun (x : nat.toSubtype) => Classical.choose ⋯) ↑(2 * n + 3) = ↑(2 * n + 4)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.P_3_3_2b [SetTheory] : nat.toSubtype → nat.toSubtype → Prop

Equations

• Chapter3.SetTheory.Set.P_3_3_2b x y = (Chapter3.SetTheory.Set.nat_equiv.symm y + 1 = Chapter3.SetTheory.Set.nat_equiv.symm x)

theorem Chapter3.SetTheory.Set.not_P_3_3_2b_existsUnique [SetTheory] : ¬∀ (x : nat.toSubtype), ∃! y : nat.toSubtype, P_3_3_2b x y

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.P_3_3_2c [SetTheory] : (nat \ {0}).toSubtype → nat.toSubtype → Prop

Equations

• Chapter3.SetTheory.Set.P_3_3_2c x y = (↑(Chapter3.SetTheory.Set.nat_equiv.symm y + 1) = ↑x)

theorem Chapter3.SetTheory.Set.P_3_3_2c_existsUnique [SetTheory] (x : (nat \ {0}).toSubtype) : ∃! y : nat.toSubtype, P_3_3_2c x y

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_2c [SetTheory] : Function (nat \ {0}) nat

Equations

• Chapter3.SetTheory.Set.f_3_3_2c = { P := Chapter3.SetTheory.Set.P_3_3_2c, unique := ⋯ }

theorem Chapter3.SetTheory.Set.f_3_3_2c_eval [SetTheory] (x : (nat \ {0}).toSubtype) (y : nat.toSubtype) : y = (fun (x : (nat \ {0}).toSubtype) => Classical.choose ⋯) x ↔ ↑(nat_equiv.symm y + 1) = ↑x

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.coe_nonzero [SetTheory] (n : ℕ) (h : n ≠ 0) : (nat \ {0}).toSubtype

Створює версію ненульового n всередині nat \ {0} для будь-якого натурального числа n.

Equations

• Chapter3.SetTheory.Set.coe_nonzero n h = ⟨↑n, ⋯⟩

theorem Chapter3.SetTheory.Set.f_3_3_2c_eval' [SetTheory] (n : ℕ) : (fun (x : (nat \ {0}).toSubtype) => Classical.choose ⋯) (coe_nonzero (n + 1) ⋯) = ↑n

theorem Chapter3.SetTheory.Set.f_3_3_2c_eval'' [SetTheory] : (fun (x : (nat \ {0}).toSubtype) => Classical.choose ⋯) (coe_nonzero 4 ⋯) = 3

theorem Chapter3.SetTheory.Set.f_3_3_2c_eval''' [SetTheory] (n : ℕ) : (fun (x : (nat \ {0}).toSubtype) => Classical.choose ⋯) (coe_nonzero (2 * n + 3) ⋯) = ↑(2 * n + 2)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.P_3_3_4 [SetTheory] : nat.toSubtype → nat.toSubtype → Prop

Приклад 3.3.4. Невикористана змінна _x підкреслена, щоб уникнути спрацьовування лінтера.

Equations

• Chapter3.SetTheory.Set.P_3_3_4 _x y = (y = 7)

theorem Chapter3.SetTheory.Set.P_3_3_4_existsUnique [SetTheory] (x : nat.toSubtype) : ∃! y : nat.toSubtype, P_3_3_4 x y

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_4 [SetTheory] : Function nat nat

Equations

• Chapter3.SetTheory.Set.f_3_3_4 = { P := Chapter3.SetTheory.Set.P_3_3_4, unique := ⋯ }

theorem Chapter3.SetTheory.Set.f_3_3_4_eval [SetTheory] (x : nat.toSubtype) : (fun (x : nat.toSubtype) => Classical.choose ⋯) x = 7

theorem Chapter3.Function.eq_iff [SetTheory] {X Y : Set} (f g : Function X Y) : f = g ↔ ∀ (x : X.toSubtype), (fun (x : X.toSubtype) => Classical.choose ⋯) x = (fun (x : X.toSubtype) => Classical.choose ⋯) x

Визначення 3.3.7 (Рівність функцій)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_8a [SetTheory] : Function nat nat

Приклад 3.3.8 (спрощений). Другу частину прикладу складно відтворити в цьому формалізмі, тому натомість цього пропонується замінник із Mathlib.

Equations

• Chapter3.SetTheory.Set.f_3_3_8a = Chapter3.Function.mk_fn fun (x : Chapter3.nat.toSubtype) => ↑(Chapter3.SetTheory.Set.nat_equiv.symm x ^ 2 + 2 * Chapter3.SetTheory.Set.nat_equiv.symm x + 1)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_8b [SetTheory] : Function nat nat

Equations

• Chapter3.SetTheory.Set.f_3_3_8b = Chapter3.Function.mk_fn fun (x : Chapter3.nat.toSubtype) => ↑((Chapter3.SetTheory.Set.nat_equiv.symm x + 1) ^ 2)

theorem Chapter3.SetTheory.Set.f_3_3_8_eq [SetTheory] : f_3_3_8a = f_3_3_8b

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_9 [SetTheory] (X : Set) : Function ∅ X

Приклад 3.3.9

Equations

• X.f_3_3_9 = { P := fun (x : ∅.toSubtype) (x : X.toSubtype) => True, unique := ⋯ }

theorem Chapter3.SetTheory.Set.empty_function_unique [SetTheory] {X : Set} (f g : Function ∅ X) : f = g

@[reducible, inline]

noncomputable abbrev Chapter3.Function.comp [SetTheory] {X Y Z : Set} (g : Function Y Z) (f : Function X Y) : Function X Z

Визначення 3.3.10 (Композиція)

Equations

• g○f = Chapter3.Function.mk_fn fun (x : X.toSubtype) => (fun (x : Y.toSubtype) => Classical.choose ⋯) ((fun (x : X.toSubtype) => Classical.choose ⋯) x)

def Chapter3.«term_○_» : Lean.TrailingParserDescr

Equations

• Chapter3.«term_○_» = Lean.ParserDescr.trailingNode `Chapter3.«term_○_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "○") (Lean.ParserDescr.cat `term 91))

theorem Chapter3.Function.comp_eval [SetTheory] {X Y Z : Set} (g : Function Y Z) (f : Function X Y) (x : X.toSubtype) : (fun (x : X.toSubtype) => Classical.choose ⋯) x = (fun (x : Y.toSubtype) => Classical.choose ⋯) ((fun (x : X.toSubtype) => Classical.choose ⋯) x)

theorem Chapter3.Function.comp_eq_comp [SetTheory] {X Y Z : Set} (g : Function Y Z) (f : Function X Y) : (g○f).to_fn = g.to_fn ∘ f.to_fn

Сумісність з операцією композиції Mathlib. Вам можуть бути корисними тактики ext та simp.

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_11 [SetTheory] : Function nat nat

Приклад 3.3.11

Equations

• Chapter3.SetTheory.Set.f_3_3_11 = Chapter3.Function.mk_fn fun (x : Chapter3.nat.toSubtype) => ↑(2 * Chapter3.SetTheory.Set.nat_equiv.symm x)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.g_3_3_11 [SetTheory] : Function nat nat

Equations

• Chapter3.SetTheory.Set.g_3_3_11 = Chapter3.Function.mk_fn fun (x : Chapter3.nat.toSubtype) => ↑(Chapter3.SetTheory.Set.nat_equiv.symm x + 3)

theorem Chapter3.SetTheory.Set.g_circ_f_3_3_11 [SetTheory] : g_3_3_11○f_3_3_11 = Function.mk_fn fun (x : nat.toSubtype) => ↑(2 * nat_equiv.symm x + 3)

theorem Chapter3.SetTheory.Set.f_circ_g_3_3_11 [SetTheory] : f_3_3_11○g_3_3_11 = Function.mk_fn fun (x : nat.toSubtype) => ↑(2 * nat_equiv.symm x + 6)

theorem Chapter3.SetTheory.Set.comp_assoc [SetTheory] {W X Y Z : Set} (h : Function Y Z) (g : Function X Y) (f : Function W X) : h○(g○f) = (h○g)○f

Лема 3.3.12 (Композиція асоціативна)

@[reducible, inline]

abbrev Chapter3.Function.one_to_one [SetTheory] {X Y : Set} (f : Function X Y) : Prop

Equations

• f.one_to_one = ∀ (x x' : X.toSubtype), x ≠ x' → (fun (x : X.toSubtype) => Classical.choose ⋯) x ≠ (fun (x : X.toSubtype) => Classical.choose ⋯) x'

theorem Chapter3.Function.one_to_one_iff [SetTheory] {X Y : Set} (f : Function X Y) : f.one_to_one ↔ ∀ (x x' : X.toSubtype), (fun (x : X.toSubtype) => Classical.choose ⋯) x = (fun (x : X.toSubtype) => Classical.choose ⋯) x' → x = x'

theorem Chapter3.Function.one_to_one_iff' [SetTheory] {X Y : Set} (f : Function X Y) : f.one_to_one ↔ Function.Injective f.to_fn

Сумісність із Mathlib-івським Function.Injective. Можливо, ви захочете скористатися тактикою unfold, щоб зрозуміти такі концепції Mathlib, як Function.Injective.

theorem Chapter3.SetTheory.Set.f_3_3_15_one_to_one [SetTheory] : (Function.mk_fn fun (n : nat.toSubtype) => ↑(nat_equiv.symm n ^ 2)).one_to_one

Приклад 3.3.15. Одна половина прикладу вимагає цілих чисел, тому виражається за допомогою функцій Mathlib замість функцій із Розділу 3.

theorem Chapter3.SetTheory.Set.two_to_one [SetTheory] {X Y : Set} {f : Function X Y} (h : ¬f.one_to_one) : ∃ (x : X.toSubtype) (x' : X.toSubtype), x ≠ x' ∧ (fun (x : X.toSubtype) => Classical.choose ⋯) x = (fun (x : X.toSubtype) => Classical.choose ⋯) x'

Ремарка 3.3.16

@[reducible, inline]

abbrev Chapter3.Function.onto [SetTheory] {X Y : Set} (f : Function X Y) : Prop

Визначення 3.3.17 (Сур'єктивні функції)

Equations

• f.onto = ∀ (y : Y.toSubtype), ∃ (x : X.toSubtype), (fun (x : X.toSubtype) => Classical.choose ⋯) x = y

theorem Chapter3.Function.onto_iff [SetTheory] {X Y : Set} (f : Function X Y) : f.onto ↔ Function.Surjective f.to_fn

Сумісність із Mathlib-івським Function.Surjective

@[reducible, inline]

abbrev Chapter3.A_3_3_18 : Type

Equations

• Chapter3.A_3_3_18 = { m : ℤ // ∃ (n : ℤ), m = n ^ 2 }

@[reducible, inline]

abbrev Chapter3.Function.bijective [SetTheory] {X Y : Set} (f : Function X Y) : Prop

Визначення 3.3.20 (Бієктивні функції)

Equations

• f.bijective = (f.one_to_one ∧ f.onto)

theorem Chapter3.Function.bijective_iff [SetTheory] {X Y : Set} (f : Function X Y) : f.bijective ↔ Function.Bijective f.to_fn

Сумісність із Mathlib-івським Function.Bijective

@[reducible, inline]

abbrev Chapter3.f_3_3_21 : Fin 3 → ↑{3, 4}

Приклад 3.3.21 (використовуючи Mathlib)

Equations

• Chapter3.f_3_3_21 0 = ⟨3, Chapter3.f_3_3_21._proof_4⟩
• Chapter3.f_3_3_21 1 = ⟨3, Chapter3.f_3_3_21._proof_4⟩
• Chapter3.f_3_3_21 2 = ⟨4, Chapter3.f_3_3_21._proof_5⟩

@[reducible, inline]

abbrev Chapter3.g_3_3_21 : Fin 2 → ↑{2, 3, 4}

Equations

• Chapter3.g_3_3_21 0 = ⟨2, Chapter3.g_3_3_21._proof_6⟩
• Chapter3.g_3_3_21 1 = ⟨3, Chapter3.g_3_3_21._proof_7⟩

@[reducible, inline]

abbrev Chapter3.h_3_3_21 : Fin 3 → ↑{3, 4, 5}

Equations

• Chapter3.h_3_3_21 0 = ⟨3, Chapter3.h_3_3_21._proof_8⟩
• Chapter3.h_3_3_21 1 = ⟨4, Chapter3.h_3_3_21._proof_9⟩
• Chapter3.h_3_3_21 2 = ⟨5, Chapter3.h_3_3_21._proof_10⟩

theorem Chapter3.Function.bijective_incorrect_def [SetTheory] : ∃ (X : Set) (Y : Set) (f : Function X Y), (∀ (x : X.toSubtype), ∃! y : Y.toSubtype, y = (fun (x : X.toSubtype) => Classical.choose ⋯) x) ∧ ¬f.bijective

Ремарка 3.3.24

@[reducible, inline]

abbrev Chapter3.Function.inverse [SetTheory] {X Y : Set} (f : Function X Y) (h : f.bijective) : Function Y X

Ми не можемо використовувати позначення f⁻¹ для оберненої функції, оскільки в класі Inv Mathlib-у обернена функція f повинна бути точно такого ж типу, як f, а Function Y X має інший тип, ніж Function X Y.

Equations

• f.inverse h = { P := fun (y : Y.toSubtype) (x : X.toSubtype) => (fun (x : X.toSubtype) => Classical.choose ⋯) x = y, unique := ⋯ }

theorem Chapter3.Function.inverse_eval [SetTheory] {X Y : Set} {f : Function X Y} (h : f.bijective) (y : Y.toSubtype) (x : X.toSubtype) : x = (fun (x : Y.toSubtype) => Classical.choose ⋯) y ↔ (fun (x : X.toSubtype) => Classical.choose ⋯) x = y

theorem Chapter3.Function.inverse_eq [SetTheory] {X Y : Set} [Nonempty X.toSubtype] {f : Function X Y} (h : f.bijective) : (f.inverse h).to_fn = Function.invFun f.to_fn

Сумісність із Mathlib-овським поняттям інверсивності

theorem Chapter3.Function.refl [SetTheory] {X Y : Set} (f : Function X Y) : f = f

Вправа 3.3.1

theorem Chapter3.Function.symm [SetTheory] {X Y : Set} (f g : Function X Y) : f = g ↔ g = f

theorem Chapter3.Function.trans [SetTheory] {X Y : Set} {f g h : Function X Y} (hfg : f = g) (hgh : g = h) : f = h

theorem Chapter3.Function.comp_congr [SetTheory] {X Y Z : Set} {f f' : Function X Y} (hff' : f = f') {g g' : Function Y Z} (hgg' : g = g') : g○f = g'○f'

theorem Chapter3.Function.comp_of_inj [SetTheory] {X Y Z : Set} {f : Function X Y} {g : Function Y Z} (hf : f.one_to_one) (hg : g.one_to_one) : (g○f).one_to_one

Вправа 3.3.2

theorem Chapter3.Function.comp_of_surj [SetTheory] {X Y Z : Set} {f : Function X Y} {g : Function Y Z} (hf : f.onto) (hg : g.onto) : (g○f).onto

theorem Chapter3.Function.comp_cancel_left [SetTheory] {X Y Z : Set} {f f' : Function X Y} {g : Function Y Z} (heq : g○f = g○f') (hg : g.one_to_one) : f = f'

Вправа 3.3.4. Сформулюйте та доведіть теореми або контрприклади у випадку, якщо hg або hf пропущені як гіпотези.

theorem Chapter3.Function.comp_cancel_right [SetTheory] {X Y Z : Set} {f : Function X Y} {g g' : Function Y Z} (heq : g○f = g'○f) (hf : g.onto) : g = g'

theorem Chapter3.Function.comp_injective [SetTheory] {X Y Z : Set} {f : Function X Y} {g : Function Y Z} (hinj : (g○f).one_to_one) : f.one_to_one

Вправа 3.3.5. Наведіть або доведіть теореми чи контрприклади у випадку, якщо f замінено на g або навпаки у висновку.

theorem Chapter3.Function.comp_surjective [SetTheory] {X Y Z : Set} {f : Function X Y} {g : Function Y Z} (hinj : (g○f).onto) : g.onto

theorem Chapter3.Function.inverse_comp_self [SetTheory] {X Y : Set} {f : Function X Y} (h : f.bijective) (x : X.toSubtype) : (fun (x : Y.toSubtype) => Classical.choose ⋯) ((fun (x : X.toSubtype) => Classical.choose ⋯) x) = x

Вправа 3.3.6

theorem Chapter3.Function.self_comp_inverse [SetTheory] {X Y : Set} {f : Function X Y} (h : f.bijective) (y : Y.toSubtype) : (fun (x : X.toSubtype) => Classical.choose ⋯) ((fun (x : Y.toSubtype) => Classical.choose ⋯) y) = y

theorem Chapter3.Function.inverse_bijective [SetTheory] {X Y : Set} {f : Function X Y} (h : f.bijective) : (f.inverse h).bijective

theorem Chapter3.Function.inverse_inverse [SetTheory] {X Y : Set} {f : Function X Y} (h : f.bijective) : (f.inverse h).inverse ⋯ = f

theorem Chapter3.Function.comp_bijective [SetTheory] {X Y Z : Set} {f : Function X Y} {g : Function Y Z} (hf : f.bijective) (hg : g.bijective) : (g○f).bijective

theorem Chapter3.Function.inv_of_comp [SetTheory] {X Y Z : Set} {f : Function X Y} {g : Function Y Z} (hf : f.bijective) (hg : g.bijective) : (g○f).inverse ⋯ = f.inverse hf○g.inverse hg

Вправа 3.3.7

@[reducible, inline]

abbrev Chapter3.Function.inclusion [SetTheory] {X Y : Set} (h : X ⊆ Y) : Function X Y

Вправа 3.3.8

Equations

• Chapter3.Function.inclusion h = Chapter3.Function.mk_fn fun (x : X.toSubtype) => ⟨↑x, ⋯⟩

@[reducible, inline]

abbrev Chapter3.Function.id [SetTheory] (X : Set) : Function X X

Equations

• Chapter3.Function.id X = Chapter3.Function.mk_fn fun (x : X.toSubtype) => x

theorem Chapter3.Function.inclusion_id [SetTheory] (X : Set) : inclusion ⋯ = id X

theorem Chapter3.Function.inclusion_comp [SetTheory] (X Y Z : Set) (hXY : X ⊆ Y) (hYZ : Y ⊆ Z) : inclusion hYZ○inclusion hXY = inclusion ⋯

theorem Chapter3.Function.comp_id [SetTheory] {A B : Set} (f : Function A B) : f○id A = f

theorem Chapter3.Function.id_comp [SetTheory] {A B : Set} (f : Function A B) : id B○f = f

theorem Chapter3.Function.comp_inv [SetTheory] {A B : Set} (f : Function A B) (hf : f.bijective) : f○f.inverse hf = id B

theorem Chapter3.Function.inv_comp [SetTheory] {A B : Set} (f : Function A B) (hf : f.bijective) : f.inverse hf○f = id A

theorem Chapter3.Function.glue [SetTheory] {X Y Z : Set} (hXY : Disjoint X Y) (f : Function X Z) (g : Function Y Z) : ∃! h : Function (X ∪ Y) Z, h○inclusion ⋯ = f ∧ h○inclusion ⋯ = g