Аналіз 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.)
• Основні властивості та операції над функціями, такі як композиція, ін'єктивні функції, сур'єктивні функції, та обернені функції.

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

Тут ми працюватимемо з версією Nat натуральних чисел, що є внутрішньою для теорії множин з Розділу 3, хоча зазвичай ми використовуватимемо перетворення, щоб одразу ж перетворити їх на натуральні числа ℕ з Mathlib.

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

• (Додайте підказку тут)

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

Визначення 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 def Chapter3.Function.to_fn [SetTheory] {X Y : Set} (f : Function X Y) : X.toSubtype → Y.toSubtype

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

Equations

• f.to_fn x = ⋯.choose

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

Equations

• Chapter3.Function.inst_coefn X Y = { coe := Chapter3.Function.to_fn }

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

@[reducible, inline]

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

Перетворення функції Mathlib на Function з Розділу 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 = f.to_fn 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) : (mk_fn f).to_fn x = f x

@[reducible, inline]

abbrev Chapter3.P_3_3_3a [SetTheory] : Nat.toSubtype → Nat.toSubtype → Prop

Приклад 3.3.3.

Equations

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

theorem Chapter3.SetTheory.Set.P_3_3_3a_existsUnique [SetTheory] (x : Nat.toSubtype) : ∃! y : Nat.toSubtype, P_3_3_3a x y

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_3a [SetTheory] : Function Nat Nat

Equations

• Chapter3.SetTheory.Set.f_3_3_3a = { P := Chapter3.P_3_3_3a, unique := ⋯ }

theorem Chapter3.SetTheory.Set.f_3_3_3a_eval [SetTheory] (x y : Nat.toSubtype) : y = f_3_3_3a.to_fn x ↔ nat_equiv.symm y = nat_equiv.symm x + 1

theorem Chapter3.SetTheory.Set.f_3_3_3a_eval' [SetTheory] (n : ℕ) : f_3_3_3a.to_fn ↑n = ↑(n + 1)

theorem Chapter3.SetTheory.Set.f_3_3_3a_eval'' [SetTheory] : f_3_3_3a.to_fn 4 = 5

theorem Chapter3.SetTheory.Set.f_3_3_3a_eval''' [SetTheory] (n : ℕ) : f_3_3_3a.to_fn ↑(2 * n + 3) = ↑(2 * n + 4)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.P_3_3_3b [SetTheory] : Nat.toSubtype → Nat.toSubtype → Prop

Equations

• Chapter3.SetTheory.Set.P_3_3_3b 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_3b_existsUnique [SetTheory] : ¬∀ (x : Nat.toSubtype), ∃! y : Nat.toSubtype, P_3_3_3b x y

@[reducible, inline]

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

Equations

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

theorem Chapter3.SetTheory.Set.P_3_3_3c_existsUnique [SetTheory] (x : (Nat \ {0}).toSubtype) : ∃! y : Nat.toSubtype, P_3_3_3c x y

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_3c [SetTheory] : Function (Nat \ {0}) Nat

Equations

• Chapter3.SetTheory.Set.f_3_3_3c = { P := Chapter3.SetTheory.Set.P_3_3_3c, unique := ⋯ }

theorem Chapter3.SetTheory.Set.f_3_3_3c_eval [SetTheory] (x : (Nat \ {0}).toSubtype) (y : Nat.toSubtype) : y = f_3_3_3c.to_fn 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_3c_eval' [SetTheory] (n : ℕ) : f_3_3_3c.to_fn (coe_nonzero (n + 1) ⋯) = ↑n

theorem Chapter3.SetTheory.Set.f_3_3_3c_eval'' [SetTheory] : f_3_3_3c.to_fn (coe_nonzero 4 ⋯) = 3

theorem Chapter3.SetTheory.Set.f_3_3_3c_eval''' [SetTheory] (n : ℕ) : f_3_3_3c.to_fn (coe_nonzero (2 * n + 3) ⋯) = ↑(2 * n + 2)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.P_3_3_5 [SetTheory] : Nat.toSubtype → Nat.toSubtype → Prop

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

Equations

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

theorem Chapter3.SetTheory.Set.P_3_3_5_existsUnique [SetTheory] (x : Nat.toSubtype) : ∃! y : Nat.toSubtype, P_3_3_5 x y

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_5 [SetTheory] : Function Nat Nat

Equations

• Chapter3.SetTheory.Set.f_3_3_5 = { P := Chapter3.SetTheory.Set.P_3_3_5, unique := ⋯ }

theorem Chapter3.SetTheory.Set.f_3_3_5_eval [SetTheory] (x : Nat.toSubtype) : f_3_3_5.to_fn x = 7

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

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

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.f_3_3_10a [SetTheory] : Function Nat Nat

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

Equations

• Chapter3.SetTheory.Set.f_3_3_10a = 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_10b [SetTheory] : Function Nat Nat

Equations

• Chapter3.SetTheory.Set.f_3_3_10b = 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_10_eq [SetTheory] : f_3_3_10a = f_3_3_10b

@[reducible, inline]

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

Приклад 3.3.11

Equations

• X.f_3_3_11 = { 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.13 (Композиція)

Equations

• g○f = Chapter3.Function.mk_fn fun (x : X.toSubtype) => g.to_fn (f.to_fn 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) : (g○f).to_fn x = g.to_fn (f.to_fn 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_14 [SetTheory] : Function Nat Nat

Приклад 3.3.14

Equations

• Chapter3.SetTheory.Set.f_3_3_14 = 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_14 [SetTheory] : Function Nat Nat

Equations

• Chapter3.SetTheory.Set.g_3_3_14 = 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_14 [SetTheory] : g_3_3_14○f_3_3_14 = Function.mk_fn fun (x : Nat.toSubtype) => ↑(2 * nat_equiv.symm x + 3)

theorem Chapter3.SetTheory.Set.f_circ_g_3_3_14 [SetTheory] : f_3_3_14○g_3_3_14 = 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.15 (Композиція асоціативна)

@[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' → f.to_fn x ≠ f.to_fn x'

theorem Chapter3.Function.one_to_one_iff [SetTheory] {X Y : Set} (f : Function X Y) : f.one_to_one ↔ ∀ (x x' : X.toSubtype), f.to_fn x = f.to_fn 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_18_one_to_one [SetTheory] : (Function.mk_fn fun (n : Nat.toSubtype) => ↑(nat_equiv.symm n ^ 2)).one_to_one

Приклад 3.3.18. Одна половина прикладу вимагає цілих чисел, тому виражається за допомогою функцій 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' ∧ f.to_fn x = f.to_fn x'

Ремарка 3.3.19

@[reducible, inline]

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

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

Equations

• f.onto = ∀ (y : Y.toSubtype), ∃ (x : X.toSubtype), f.to_fn 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_21 : Type

Equations

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

@[reducible, inline]

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

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

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_24 : Fin 3 → ↑{3, 4}

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

Equations

• Chapter3.f_3_3_24 0 = ⟨3, Chapter3.f_3_3_24._proof_1⟩
• Chapter3.f_3_3_24 1 = ⟨3, Chapter3.f_3_3_24._proof_1⟩
• Chapter3.f_3_3_24 2 = ⟨4, Chapter3.f_3_3_24._proof_2⟩

@[reducible, inline]

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

Equations

• Chapter3.g_3_3_24 0 = ⟨2, Chapter3.g_3_3_24._proof_1⟩
• Chapter3.g_3_3_24 1 = ⟨3, Chapter3.g_3_3_24._proof_2⟩

@[reducible, inline]

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

Equations

• Chapter3.h_3_3_24 0 = ⟨3, Chapter3.h_3_3_24._proof_1⟩
• Chapter3.h_3_3_24 1 = ⟨4, Chapter3.h_3_3_24._proof_2⟩
• Chapter3.h_3_3_24 2 = ⟨5, Chapter3.h_3_3_24._proof_3⟩

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

Ремарка 3.3.27

@[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) => f.to_fn 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 = (f.inverse h).to_fn y ↔ f.to_fn 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. Хоча доведення, що безпосередньо оперує функціями, було б коротшим, суть вправи полягає в тому, щоб показати це, використовуючи визначення Function.eq_iff.

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.empty_function_one_to_one_iff [SetTheory] (X : Set) (f : Function ∅ X) : f.one_to_one ↔ sorry

Вправа 3.3.3 - заповніть sorry у твердженнях розумним чином.

theorem Chapter3.empty_function_onto_iff [SetTheory] (X : Set) (f : Function ∅ X) : f.onto ↔ sorry

theorem Chapter3.empty_function_bijective_iff [SetTheory] (X : Set) (f : Function ∅ X) : f.bijective ↔ sorry

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.

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 : f.onto) : g = g'

def Chapter3.Function.comp_cancel_left_without_hg [SetTheory] : Decidable (∀ (X Y Z : Set) (f f' : Function X Y) (g : Function Y Z), g○f = g○f' → f = f')

Equations

• Chapter3.Function.comp_cancel_left_without_hg = sorry

def Chapter3.Function.comp_cancel_right_without_hg [SetTheory] : Decidable (∀ (X Y Z : Set) (f : Function X Y) (g g' : Function Y Z), g○f = g'○f → g = g')

Equations

• Chapter3.Function.comp_cancel_right_without_hg = sorry

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.

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

def Chapter3.Function.comp_injective' [SetTheory] : Decidable (∀ (X Y Z : Set) (f : Function X Y) (g : Function Y Z), (g○f).one_to_one → g.one_to_one)

Equations

• Chapter3.Function.comp_injective' = sorry

def Chapter3.Function.comp_surjective' [SetTheory] : Decidable (∀ (X Y Z : Set) (f : Function X Y) (g : Function Y Z), (g○f).onto → f.onto)

Equations

• Chapter3.Function.comp_surjective' = sorry

theorem Chapter3.Function.inverse_comp_self [SetTheory] {X Y : Set} {f : Function X Y} (h : f.bijective) (x : X.toSubtype) : (f.inverse h).to_fn (f.to_fn 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) : f.to_fn ((f.inverse h).to_fn 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

Вправа 3.3.7

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

@[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

theorem Chapter3.Function.glue' [SetTheory] {X Y Z : Set} (f : Function X Z) (g : Function Y Z) (hfg : ∀ (x : (X ∩ Y).toSubtype), f.to_fn ⟨↑x, ⋯⟩ = g.to_fn ⟨↑x, ⋯⟩) : ∃! h : Function (X ∪ Y) Z, h○inclusion ⋯ = f ∧ h○inclusion ⋯ = g