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

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

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

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

namespace Chapter3/- Тут ми працюватимемо з версією `nat` натуральних чисел, що є внутрішньою для теорії множин з Розділу 3, хоча зазвичай ми використовуватимемо перетворення, щоб одразу ж перетворити їх на натуральні числа із Mathlib - `ℕ`. -/ export SetTheory (Set Object nat)variable [SetTheory]

Визначення 3.3.1. unknown identifier 'Function'Function X Y — це структура функцій із unknown identifier 'X'X до unknown identifier 'Y'Y. Аналогічно типу Mathlib unknown identifier 'X'sorry → sorry : Sort (imax u_1 u_2)X → unknown identifier 'Y'Y.

@[ext] structure Function (X Y: Set) where P : X → Y → Prop unique : ∀ x: X, ∃! y: Y, P x y
Chapter3.Function.mk [SetTheory] {X Y : Set} (P : X.toSubtype → Y.toSubtype → Prop) (unique : ∀ (x : X.toSubtype), ∃! y, P x y) : Function X Y#check Function.mk
Chapter3.Function.mk [SetTheory] {X Y : Set} (P : X.toSubtype → Y.toSubtype → Prop)
  (unique : ∀ (x : X.toSubtype), ∃! y, P x y) : Function X Y

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

noncomputable instance Function.inst_coefn (X Y: Set) : CoeFun (Function X Y) (fun _ ↦ X → Y) where coe := fun f x ↦ Classical.choose (f.unique x)
noncomputable abbrev Function.to_fn {X Y: Set} (f: Function X Y) (x:X) : Y := f xtheorem Function.to_fn_eval {X Y: Set} (f: Function X Y) (x:X) : f.to_fn x = f x := rfl

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

abbrev Function.mk_fn {X Y: Set} (f: X → Y) : Function X Y := Function.mk (fun x y ↦ y = f x) (inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtype⊢ ∀ (x : X.toSubtype), ∃! y, (fun x y => y = f x) x y inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtype⊢ ∃! y, (fun x y => y = f x) x y inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtype⊢ (fun x y => y = f x) x (f x)inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtype⊢ ∀ (y : Y.toSubtype), (fun x y => y = f x) x y → y = f x inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtype⊢ (fun x y => y = f x) x (f x) All goals completed! 🐙 inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtypey:Y.toSubtypeh:(fun x y => y = f x) x y⊢ y = f x All goals completed! 🐙)

Визначення 3.3.1

theorem Function.eval {X Y: Set} (f: Function X Y) (x: X) (y: Y) : y = f x ↔ f.P x y := inst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypey:Y.toSubtype⊢ y = (fun x => Classical.choose ⋯) x ↔ f.P x y inst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypey:Y.toSubtype⊢ y = (fun x => Classical.choose ⋯) x → f.P x yinst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypey:Y.toSubtype⊢ f.P x y → y = (fun x => Classical.choose ⋯) x inst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypey:Y.toSubtype⊢ y = (fun x => Classical.choose ⋯) x → f.P x y inst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypey:Y.toSubtypeh:y = (fun x => Classical.choose ⋯) x⊢ f.P x y inst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtype⊢ f.P x ((fun x => Classical.choose ⋯) x) All goals completed! 🐙 inst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypey:Y.toSubtypeh:f.P x y⊢ y = (fun x => Classical.choose ⋯) x inst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypey:Y.toSubtypeh:f.P x y⊢ f.P x y All goals completed! 🐙
@[simp] theorem Function.eval_of {X Y: Set} (f: X → Y) (x:X) : (Function.mk_fn f) x = f x := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtype⊢ (fun x => Classical.choose ⋯) x = f x inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtype⊢ f x = (fun x => Classical.choose ⋯) x; All goals completed! 🐙

Приклад 3.3.2.

abbrev P_3_3_2a : nat → nat → Prop := fun x y ↦ (y:ℕ) = (x:ℕ)+1
theorem SetTheory.Set.P_3_3_2a_existsUnique (x: nat) : ∃! y: nat, P_3_3_2a x y := inst✝:SetTheoryx:nat.toSubtype⊢ ∃! y, P_3_3_2a x y inst✝:SetTheoryx:nat.toSubtype⊢ P_3_3_2a x ↑(nat_equiv.symm x + 1)inst✝:SetTheoryx:nat.toSubtype⊢ ∀ (y : nat.toSubtype), P_3_3_2a x y → y = ↑(nat_equiv.symm x + 1) inst✝:SetTheoryx:nat.toSubtype⊢ P_3_3_2a x ↑(nat_equiv.symm x + 1) All goals completed! 🐙 inst✝:SetTheoryx:nat.toSubtypey:nat.toSubtypeh:P_3_3_2a x y⊢ y = ↑(nat_equiv.symm x + 1) inst✝:SetTheoryx:nat.toSubtypey:nat.toSubtypeh:y = nat_equiv (nat_equiv.symm x + 1)⊢ y = ↑(nat_equiv.symm x + 1) All goals completed! 🐙abbrev SetTheory.Set.f_3_3_2a : Function nat nat := Function.mk P_3_3_2a P_3_3_2a_existsUniquetheorem SetTheory.Set.f_3_3_2a_eval (x y: nat) : y = f_3_3_2a x ↔ (y:ℕ) = (x+1:ℕ) := Function.eval _ _ _theorem SetTheory.Set.f_3_3_2a_eval' (n: ℕ) : f_3_3_2a (n:nat) = (n+1:ℕ) := inst✝:SetTheoryn:ℕ⊢ (fun x => Classical.choose ⋯) ↑n = ↑(n + 1) inst✝:SetTheoryn:ℕ⊢ ↑(n + 1) = (fun x => Classical.choose ⋯) ↑n All goals completed! 🐙theorem SetTheory.Set.f_3_3_2a_eval'' : f_3_3_2a 4 = 5 := f_3_3_2a_eval' 4theorem SetTheory.Set.f_3_3_2a_eval''' (n:ℕ) : f_3_3_2a (2*n+3: ℕ) = (2*n+4:ℕ) := inst✝:SetTheoryn:ℕ⊢ (fun x => Classical.choose ⋯) ↑(2 * n + 3) = ↑(2 * n + 4) All goals completed! 🐙abbrev SetTheory.Set.P_3_3_2b : nat → nat → Prop := fun x y ↦ (y+1:ℕ) = (x:ℕ)theorem SetTheory.Set.not_P_3_3_2b_existsUnique : ¬ ∀ x, ∃! y: nat, P_3_3_2b x y := inst✝:SetTheory⊢ ¬∀ (x : nat.toSubtype), ∃! y, P_3_3_2b x y inst✝:SetTheoryh:∀ (x : nat.toSubtype), ∃! y, P_3_3_2b x y⊢ False inst✝:SetTheoryh:∃ x, P_3_3_2b 0 x⊢ False inst✝:SetTheoryn:nat.toSubtypehn:P_3_3_2b 0 n⊢ False have : ((0:nat):ℕ) = 0 := inst✝:SetTheory⊢ ¬∀ (x : nat.toSubtype), ∃! y, P_3_3_2b x y All goals completed! 🐙 All goals completed! 🐙abbrev SetTheory.Set.P_3_3_2c : (nat \ {(0:Object)}: Set) → nat → Prop := fun x y ↦ ((y+1:ℕ):Object) = xtheorem SetTheory.Set.P_3_3_2c_existsUnique (x: (nat \ {(0:Object)}: Set)) : ∃! y: nat, P_3_3_2c x y := inst✝:SetTheoryx:(nat \ {0}).toSubtype⊢ ∃! y, P_3_3_2c x y -- Тут йде деяке технічне розпакування пов'язане з тонкими відмінностями між типом `Object`, -- множинами, перетвореними на підтипи `Object`, та підмножинами цих множин. inst✝:SetTheoryx:Objecthx:x ∈ nat \ {0}⊢ ∃! y, P_3_3_2c ⟨x, hx⟩ y inst✝:SetTheoryx:Objecthx✝:x ∈ nat \ {0}hx:x ∈ nat ∧ ¬x = 0⊢ ∃! y, P_3_3_2c ⟨x, hx✝⟩ y inst✝:SetTheoryx:Objecthx:x ∈ nat \ {0}hx1:x ∈ nathx2:¬x = 0⊢ ∃! y, P_3_3_2c ⟨x, hx⟩ y inst✝:SetTheoryx:Objecthx:x ∈ nat \ {0}hx1:x ∈ nathx2:¬x = 0n:ℕ := nat_equiv.symm ⟨x, hx1⟩⊢ ∃! y, P_3_3_2c ⟨x, hx⟩ y have : x = (n:nat) := inst✝:SetTheoryx:(nat \ {0}).toSubtype⊢ ∃! y, P_3_3_2c x y All goals completed! 🐙 inst✝:SetTheoryx:Objecthx:x ∈ nat \ {0}hx1:x ∈ natn:ℕ := nat_equiv.symm ⟨x, hx1⟩this:x = ↑↑nhx2:¬n = 0⊢ ∃! y, nat_equiv.symm y + 1 = n replace hx2 : n = (n-1) + 1 := inst✝:SetTheoryx:(nat \ {0}).toSubtype⊢ ∃! y, P_3_3_2c x y All goals completed! 🐙 inst✝:SetTheoryx:Objecthx:x ∈ nat \ {0}hx1:x ∈ natn:ℕ := nat_equiv.symm ⟨x, hx1⟩this:x = ↑↑nhx2:n = n - 1 + 1⊢ nat_equiv.symm ↑(n - 1) + 1 = ninst✝:SetTheoryx:Objecthx:x ∈ nat \ {0}hx1:x ∈ natn:ℕ := nat_equiv.symm ⟨x, hx1⟩this:x = ↑↑nhx2:n = n - 1 + 1⊢ ∀ (y : nat.toSubtype), nat_equiv.symm y + 1 = n → y = ↑(n - 1) inst✝:SetTheoryx:Objecthx:x ∈ nat \ {0}hx1:x ∈ natn:ℕ := nat_equiv.symm ⟨x, hx1⟩this:x = ↑↑nhx2:n = n - 1 + 1⊢ nat_equiv.symm ↑(n - 1) + 1 = n All goals completed! 🐙 inst✝:SetTheoryx:Objecthx:x ∈ nat \ {0}hx1:x ∈ natn:ℕ := nat_equiv.symm ⟨x, hx1⟩this:x = ↑↑nhx2:n = n - 1 + 1y:nat.toSubtypehy:nat_equiv.symm y + 1 = n⊢ y = ↑(n - 1) inst✝:SetTheoryx:Objecthx:x ∈ nat \ {0}hx1:x ∈ natn:ℕ := nat_equiv.symm ⟨x, hx1⟩this:x = ↑↑nhx2:n = n - 1 + 1y:nat.toSubtypem:ℕ := nat_equiv.symm yhy:m + 1 = n⊢ y = ↑(n - 1) All goals completed! 🐙abbrev SetTheory.Set.f_3_3_2c : Function (nat \ {(0:Object)}: Set) nat := Function.mk P_3_3_2c P_3_3_2c_existsUniquetheorem SetTheory.Set.f_3_3_2c_eval (x: (nat \ {(0:Object)}: Set)) (y: nat) : y = f_3_3_2c x ↔ ((y+1:ℕ):Object) = x := Function.eval _ _ _

Створює версію ненульового unknown identifier 'n'n всередині unknown identifier 'nat'sorry \ {0} : ?m.128840nat \ {0} для будь-якого натурального числа n.

abbrev SetTheory.Set.coe_nonzero (n:ℕ) (h: n ≠ 0): (nat \ {(0:Object)}: Set) := ⟨((n:ℕ):Object), inst✝:SetTheoryn:ℕh:n ≠ 0⊢ ↑n ∈ nat \ {0} inst✝:SetTheoryn:ℕh:n ≠ 0⊢ ↑n ∈ nat inst✝:SetTheoryn:ℕh:n ≠ 0⊢ ↑↑n ∈ nat All goals completed! 🐙 ⟩
theorem SetTheory.Set.f_3_3_2c_eval' (n: ℕ) : f_3_3_2c (coe_nonzero (n+1) (inst✝:SetTheoryn:ℕ⊢ n + 1 ≠ 0 All goals completed! 🐙)) = n := inst✝:SetTheoryn:ℕ⊢ (fun x => Classical.choose ⋯) (coe_nonzero (n + 1) ⋯) = ↑n inst✝:SetTheoryn:ℕ⊢ ↑n = (fun x => Classical.choose ⋯) (coe_nonzero (n + 1) ⋯); inst✝:SetTheoryn:ℕ⊢ ↑(nat_equiv.symm ↑n + 1) = ↑(coe_nonzero (n + 1) ⋯); All goals completed! 🐙theorem SetTheory.Set.f_3_3_2c_eval'' : f_3_3_2c (coe_nonzero 4 (inst✝:SetTheory⊢ 4 ≠ 0 All goals completed! 🐙)) = 3 := inst✝:SetTheory⊢ (fun x => Classical.choose ⋯) (coe_nonzero 4 ⋯) = 3 All goals completed! 🐙theorem SetTheory.Set.f_3_3_2c_eval''' (n:ℕ) : f_3_3_2c (coe_nonzero (2*n+3) (inst✝:SetTheoryn:ℕ⊢ 2 * n + 3 ≠ 0 All goals completed! 🐙)) = (2*n+2:ℕ) := inst✝:SetTheoryn:ℕ⊢ (fun x => Classical.choose ⋯) (coe_nonzero (2 * n + 3) ⋯) = ↑(2 * n + 2) All goals completed! 🐙

Приклад 3.3.3 трішки складно відтворити за допомогою поточного формалізму, оскільки дійсні числа ще не побудовані. Натомість я пропоную деякі аналоги з Mathlib. Звичайно, для заповнення цих sorry знадобиться використання деякого API із Mathlib, наприклад, для невід'ємного дійсного класу NNReal : TypeNNReal, і того, як цей клас взаємодіє з ℝ : Typeℝ.

declaration uses 'sorry'example : ¬ ∃ f: ℝ → ℝ, ∀ x y, y = f x ↔ y^2 = x := inst✝:SetTheory⊢ ¬∃ f, ∀ (x y : ℝ), y = f x ↔ y ^ 2 = x All goals completed! 🐙
declaration uses 'sorry'example : ¬ ∃ f: NNReal → ℝ, ∀ x y, y = f x ↔ y^2 = x := inst✝:SetTheory⊢ ¬∃ f, ∀ (x : NNReal) (y : ℝ), y = f x ↔ y ^ 2 = ↑x All goals completed! 🐙declaration uses 'sorry'example : ∃ f: NNReal → NNReal, ∀ x y, y = f x ↔ y^2 = x := inst✝:SetTheory⊢ ∃ f, ∀ (x y : NNReal), y = f x ↔ y ^ 2 = x All goals completed! 🐙

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

abbrev SetTheory.Set.P_3_3_4 : nat → nat → Prop := fun _x y ↦ y = 7
theorem SetTheory.Set.P_3_3_4_existsUnique (x: nat) : ∃! y: nat, P_3_3_4 x y := inst✝:SetTheoryx:nat.toSubtype⊢ ∃! y, P_3_3_4 x y inst✝:SetTheoryx:nat.toSubtype⊢ P_3_3_4 x 7inst✝:SetTheoryx:nat.toSubtype⊢ ∀ (y : nat.toSubtype), P_3_3_4 x y → y = 7 all_goals All goals completed! 🐙abbrev SetTheory.Set.f_3_3_4 : Function nat nat := Function.mk P_3_3_4 P_3_3_4_existsUniquetheorem SetTheory.Set.f_3_3_4_eval (x: nat) : f_3_3_4 x = 7 := inst✝:SetTheoryx:nat.toSubtype⊢ (fun x => Classical.choose ⋯) x = 7 inst✝:SetTheoryx:nat.toSubtype⊢ 7 = (fun x => Classical.choose ⋯) x; All goals completed! 🐙

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

theorem Function.eq_iff {X Y: Set} (f g: Function X Y) : f = g ↔ ∀ x: X, f x = g x := inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g ↔ ∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g → ∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) xinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ (∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x) → f = g inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g → ∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:f = g⊢ ∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x; All goals completed! 🐙 inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x⊢ f = g inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) xx:X.toSubtypey:Y.toSubtype⊢ f.P x y ↔ g.P x y inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) xx:X.toSubtypey:Y.toSubtype⊢ f.P x y → g.P x yinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) xx:X.toSubtypey:Y.toSubtype⊢ g.P x y → f.P x y inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) xx:X.toSubtypey:Y.toSubtype⊢ f.P x y → g.P x y inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) xx:X.toSubtypey:Y.toSubtypehf:f.P x y⊢ g.P x y rwa [←Function.eval _ _ _, ←h x, Function.eval _ _ _inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) xx:X.toSubtypey:Y.toSubtypehf:f.P x y⊢ f.P x y inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) xx:X.toSubtypey:Y.toSubtypehg:g.P x y⊢ f.P x y rwa [←Function.eval _ _ _, h x, Function.eval _ _ _inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) xx:X.toSubtypey:Y.toSubtypehg:g.P x y⊢ g.P x y

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

abbrev SetTheory.Set.f_3_3_8a : Function nat nat := Function.mk_fn (fun x ↦ (x^2 + 2*x + 1:ℕ))
abbrev SetTheory.Set.f_3_3_8b : Function nat nat := Function.mk_fn (fun x ↦ ((x+1)^2:ℕ))theorem SetTheory.Set.f_3_3_8_eq : f_3_3_8a = f_3_3_8b := inst✝:SetTheory⊢ f_3_3_8a = f_3_3_8b inst✝:SetTheory⊢ ∀ (x : nat.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x inst✝:SetTheoryx:nat.toSubtype⊢ (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x inst✝:SetTheoryx:nat.toSubtype⊢ ↑(nat_equiv.symm x ^ 2 + 2 * nat_equiv.symm x + 1) = ↑((nat_equiv.symm x + 1) ^ 2) inst✝:SetTheoryx:nat.toSubtypen:ℕ := nat_equiv.symm x⊢ ↑(n ^ 2 + 2 * n + 1) = ↑((n + 1) ^ 2) inst✝:SetTheoryx:nat.toSubtypen:ℕ := nat_equiv.symm x⊢ n ^ 2 + 2 * n + 1 = (n + 1) ^ 2; All goals completed! 🐙declaration uses 'sorry'example : (fun x:NNReal ↦ (x:ℝ)) = (fun x:NNReal ↦ |(x:ℝ)|) := inst✝:SetTheory⊢ (fun x => ↑x) = fun x => |↑x| All goals completed! 🐙declaration uses 'sorry'example : (fun x:ℝ ↦ (x:ℝ)) ≠ (fun x:ℝ ↦ |(x:ℝ)|) := inst✝:SetTheory⊢ (fun x => x) ≠ fun x => |x| All goals completed! 🐙

Приклад 3.3.9

abbrev SetTheory.Set.f_3_3_9 (X:Set) : Function (∅:Set) X := Function.mk (fun _ _ ↦ True) (inst✝:SetTheoryX:Set⊢ ∀ (x : ∅.toSubtype), ∃! y, (fun x x => True) x y inst✝:SetTheoryX:Setx:Objecthx:x ∈ ∅⊢ ∃! y, (fun x x => True) ⟨x, hx⟩ y; All goals completed! 🐙)
theorem declaration uses 'sorry'SetTheory.Set.empty_function_unique {X: Set} (f g: Function (∅:Set) X) : f = g := inst✝:SetTheoryX:Setf:Function ∅ Xg:Function ∅ X⊢ f = g All goals completed! 🐙

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

noncomputable abbrev Function.comp {X Y Z: Set} (g: Function Y Z) (f: Function X Y) : Function X Z := Function.mk_fn (fun x ↦ g (f x))
-- `∘` вже використовується в Mathlib для композиції функцій Mathlib, -- тому ми використовуємо тут `○` замість цього символа, щоб уникнути неоднозначності. infix:90 "○" => Function.comptheorem Function.comp_eval {X Y Z: Set} (g: Function Y Z) (f: Function X Y) (x: X) : (g ○ f) x = g (f x) := Function.eval_of _ _

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

theorem declaration uses 'sorry'Function.comp_eq_comp {X Y Z: Set} (g: Function Y Z) (f: Function X Y) : (g ○ f).to_fn = g.to_fn ∘ f.to_fn := inst✝:SetTheoryX:SetY:SetZ:Setg:Function Y Zf:Function X Y⊢ (g○f).to_fn = g.to_fn ∘ f.to_fn All goals completed! 🐙

Приклад 3.3.11

abbrev SetTheory.Set.f_3_3_11 : Function nat nat := Function.mk_fn (fun x ↦ (2*x:ℕ))
abbrev SetTheory.Set.g_3_3_11 : Function nat nat := Function.mk_fn (fun x ↦ (x+3:ℕ))theorem SetTheory.Set.g_circ_f_3_3_11 : g_3_3_11 ○ f_3_3_11 = Function.mk_fn (fun x ↦ ((2*(x:ℕ)+3:ℕ):nat)) := inst✝:SetTheory⊢ g_3_3_11○f_3_3_11 = Function.mk_fn fun x => ↑(2 * nat_equiv.symm x + 3) inst✝:SetTheory⊢ ∀ (x : nat.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x inst✝:SetTheoryx:nat.toSubtype⊢ (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x inst✝:SetTheoryx:nat.toSubtype⊢ ↑(nat_equiv.symm ↑(2 * nat_equiv.symm x) + 3) = ↑(2 * nat_equiv.symm x + 3) All goals completed! 🐙theorem SetTheory.Set.f_circ_g_3_3_11 : f_3_3_11 ○ g_3_3_11 = Function.mk_fn (fun x ↦ ((2*(x:ℕ)+6:ℕ):nat)) := inst✝:SetTheory⊢ f_3_3_11○g_3_3_11 = Function.mk_fn fun x => ↑(2 * nat_equiv.symm x + 6) inst✝:SetTheory⊢ ∀ (x : nat.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x inst✝:SetTheoryx:nat.toSubtype⊢ (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x inst✝:SetTheoryx:nat.toSubtype⊢ ↑(2 * nat_equiv.symm ↑(nat_equiv.symm x + 3)) = ↑(2 * nat_equiv.symm x + 6) inst✝:SetTheoryx:nat.toSubtype⊢ 2 * (nat_equiv.symm x + 3) = 2 * nat_equiv.symm x + 6; All goals completed! 🐙

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

theorem SetTheory.Set.comp_assoc {W X Y Z: Set} (h: Function Y Z) (g: Function X Y) (f: Function W X) : h ○ (g ○ f) = (h ○ g) ○ f := inst✝:SetTheoryW:SetX:SetY:SetZ:Seth:Function Y Zg:Function X Yf:Function W X⊢ h○(g○f) = (h○g)○f inst✝:SetTheoryW:SetX:SetY:SetZ:Seth:Function Y Zg:Function X Yf:Function W X⊢ ∀ (x : W.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x inst✝:SetTheoryW:SetX:SetY:SetZ:Seth:Function Y Zg:Function X Yf:Function W Xx:W.toSubtype⊢ (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x All goals completed! 🐙
abbrev Function.one_to_one {X Y: Set} (f: Function X Y) : Prop := ∀ x x': X, x ≠ x' → f x ≠ f x'theorem Function.one_to_one_iff {X Y: Set} (f: Function X Y) : f.one_to_one ↔ ∀ x x': X, f x = f x' → x = x' := inst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.one_to_one ↔ ∀ (x x' : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x' → x = x' inst✝:SetTheoryX:SetY:Setf:Function X Y⊢ ∀ (a : X.toSubtype), (∀ (x' : X.toSubtype), a ≠ x' → (fun x => Classical.choose ⋯) a ≠ (fun x => Classical.choose ⋯) x') ↔ ∀ (x' : X.toSubtype), (fun x => Classical.choose ⋯) a = (fun x => Classical.choose ⋯) x' → a = x'; inst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtype⊢ (∀ (x' : X.toSubtype), x ≠ x' → (fun x => Classical.choose ⋯) x ≠ (fun x => Classical.choose ⋯) x') ↔ ∀ (x' : X.toSubtype), (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x' → x = x' inst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtype⊢ ∀ (a : X.toSubtype), x ≠ a → (fun x => Classical.choose ⋯) x ≠ (fun x => Classical.choose ⋯) a ↔ (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) a → x = a; inst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypex':X.toSubtype⊢ x ≠ x' → (fun x => Classical.choose ⋯) x ≠ (fun x => Classical.choose ⋯) x' ↔ (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x' → x = x' All goals completed! 🐙

Сумісність із Mathlib-івським Function.Injective.{u₁, u₂} {α : Sort u₁} {β : Sort u₂} (f : α → β) : PropFunction.Injective. Можливо, ви захочете скористатися тактикою unknown identifier 'unfold'unfold, щоб зрозуміти такі концепції Mathlib, як Function.Injective.{u₁, u₂} {α : Sort u₁} {β : Sort u₂} (f : α → β) : PropFunction.Injective.

theorem declaration uses 'sorry'Function.one_to_one_iff' {X Y: Set} (f: Function X Y) : f.one_to_one ↔ Function.Injective f.to_fn := inst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.one_to_one ↔ Function.Injective f.to_fn All goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.f_3_3_15_one_to_one : (Function.mk_fn (fun (n:nat) ↦ ((n^2:ℕ):nat))).one_to_one := inst✝:SetTheory⊢ (Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).one_to_one All goals completed! 🐙
declaration uses 'sorry'example : ¬ Function.Injective (fun (n:ℤ) ↦ n^2) := inst✝:SetTheory⊢ ¬Function.Injective fun n => n ^ 2 All goals completed! 🐙declaration uses 'sorry'example : Function.Injective (fun (n:ℕ) ↦ n^2) := inst✝:SetTheory⊢ Function.Injective fun n => n ^ 2 All goals completed! 🐙

Ремарка 3.3.16

theorem declaration uses 'sorry'SetTheory.Set.two_to_one {X Y: Set} {f: Function X Y} (h: ¬ f.one_to_one) : ∃ x x': X, x ≠ x' ∧ f x = f x' := inst✝:SetTheoryX:SetY:Setf:Function X Yh:¬f.one_to_one⊢ ∃ x x', x ≠ x' ∧ (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x' All goals completed! 🐙

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

abbrev Function.onto {X Y: Set} (f: Function X Y) : Prop := ∀ y: Y, ∃ x: X, f x = y

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

theorem declaration uses 'sorry'Function.onto_iff {X Y: Set} (f: Function X Y) : f.onto ↔ Function.Surjective f.to_fn := inst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.onto ↔ Function.Surjective f.to_fn All goals completed! 🐙

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

declaration uses 'sorry'example : ¬ Function.Surjective (fun (n:ℤ) ↦ n^2) := inst✝:SetTheory⊢ ¬Function.Surjective fun n => n ^ 2 All goals completed! 🐙
abbrev A_3_3_18 := { m:ℤ // ∃ n:ℤ, m = n^2 }declaration uses 'sorry'example : Function.Surjective (fun (n:ℤ) ↦ ⟨ n^2, inst✝:SetTheoryn:ℤ⊢ ∃ n_1, n ^ 2 = n_1 ^ 2 All goals completed! 🐙 ⟩ : ℤ → A_3_3_18) := inst✝:SetTheory⊢ Function.Surjective fun n => ⟨n ^ 2, ⋯⟩ All goals completed! 🐙

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

abbrev Function.bijective {X Y: Set} (f: Function X Y) : Prop := f.one_to_one ∧ f.onto

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

theorem declaration uses 'sorry'Function.bijective_iff {X Y: Set} (f: Function X Y) : f.bijective ↔ Function.Bijective f.to_fn := inst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.bijective ↔ Function.Bijective f.to_fn All goals completed! 🐙

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

abbrev f_3_3_21 : Fin 3 → ({3,4}:_root_.Set ℕ) := fun x ↦ match x with | 0 => ⟨ 3, inst✝:SetTheoryx:Fin 3⊢ 3 ∈ {3, 4} All goals completed! 🐙 ⟩ | 1 => ⟨ 3, inst✝:SetTheoryx:Fin 3⊢ 3 ∈ {3, 4} All goals completed! 🐙 ⟩ | 2 => ⟨ 4, inst✝:SetTheoryx:Fin 3⊢ 4 ∈ {3, 4} All goals completed! 🐙 ⟩
declaration uses 'sorry'example : ¬ Function.Injective f_3_3_21 := inst✝:SetTheory⊢ ¬Function.Injective f_3_3_21 All goals completed! 🐙declaration uses 'sorry'example : ¬ Function.Bijective f_3_3_21 := inst✝:SetTheory⊢ ¬Function.Bijective f_3_3_21 All goals completed! 🐙abbrev g_3_3_21 : Fin 2 → ({2,3,4}:_root_.Set ℕ) := fun x ↦ match x with | 0 => ⟨ 2, inst✝:SetTheoryx:Fin 2⊢ 2 ∈ {2, 3, 4} All goals completed! 🐙 ⟩ | 1 => ⟨ 3, inst✝:SetTheoryx:Fin 2⊢ 3 ∈ {2, 3, 4} All goals completed! 🐙 ⟩declaration uses 'sorry'example : ¬ Function.Surjective g_3_3_21 := inst✝:SetTheory⊢ ¬Function.Surjective g_3_3_21 All goals completed! 🐙declaration uses 'sorry'example : ¬ Function.Bijective g_3_3_21 := inst✝:SetTheory⊢ ¬Function.Bijective g_3_3_21 All goals completed! 🐙abbrev h_3_3_21 : Fin 3 → ({3,4,5}:_root_.Set ℕ) := fun x ↦ match x with | 0 => ⟨ 3, inst✝:SetTheoryx:Fin 3⊢ 3 ∈ {3, 4, 5} All goals completed! 🐙 ⟩ | 1 => ⟨ 4, inst✝:SetTheoryx:Fin 3⊢ 4 ∈ {3, 4, 5} All goals completed! 🐙 ⟩ | 2 => ⟨ 5, inst✝:SetTheoryx:Fin 3⊢ 5 ∈ {3, 4, 5} All goals completed! 🐙 ⟩declaration uses 'sorry'example : Function.Bijective h_3_3_21 := inst✝:SetTheory⊢ Function.Bijective h_3_3_21 All goals completed! 🐙

Приклад 3.3.22 сформульовано з використанням Mathlib, а не теорії множин, щоб уникнути деяких нудних технічних проблем (див. Вправу 3.3.2)

declaration uses 'sorry'example : Function.Bijective (fun n ↦ ⟨ n+1, inst✝:SetTheoryn:ℕ⊢ n + 1 ≠ 0 All goals completed! 🐙⟩ : ℕ → { n:ℕ // n ≠ 0 }) := inst✝:SetTheory⊢ Function.Bijective fun n => ⟨n + 1, ⋯⟩ All goals completed! 🐙
declaration uses 'sorry'example : ¬ Function.Bijective (fun n ↦ n+1) := inst✝:SetTheory⊢ ¬Function.Bijective fun n => n + 1 All goals completed! 🐙

Ремарка 3.3.24

theorem declaration uses 'sorry'Function.bijective_incorrect_def : ∃ X Y: Set, ∃ f: Function X Y, (∀ x: X, ∃! y: Y, y = f x) ∧ ¬ f.bijective := inst✝:SetTheory⊢ ∃ X Y f, (∀ (x : X.toSubtype), ∃! y, y = (fun x => Classical.choose ⋯) x) ∧ ¬f.bijective All goals completed! 🐙

Ми не можемо використовувати позначення unknown identifier 'f'sorry⁻¹ : ?m.129320f⁻¹ для оберненої функції, оскільки в класі Inv.{u} (α : Type u) : Type uInv Mathlib-у обернена функція unknown identifier 'f'f повинна бути точно такого ж типу, як unknown identifier 'f'f, а unknown identifier 'Function'Function Y X має інший тип, ніж unknown identifier 'Function'Function X Y.

abbrev Function.inverse {X Y: Set} (f: Function X Y) (h: f.bijective) : Function Y X := Function.mk (fun y x ↦ f x = y) (inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijective⊢ ∀ (x : Y.toSubtype), ∃! y, (fun y x => (fun x => Classical.choose ⋯) x = y) x y inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtype⊢ ∃! y_1, (fun y x => (fun x => Classical.choose ⋯) x = y) y y_1 inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtype⊢ ∃ x, (fun y x => (fun x => Classical.choose ⋯) x = y) y xinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtype⊢ ∀ (y₁ y₂ : X.toSubtype), (fun y x => (fun x => Classical.choose ⋯) x = y) y y₁ → (fun y x => (fun x => Classical.choose ⋯) x = y) y y₂ → y₁ = y₂ inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtype⊢ ∃ x, (fun y x => (fun x => Classical.choose ⋯) x = y) y x inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtypex:X.toSubtypehx:(fun x => Classical.choose ⋯) x = y⊢ ∃ x, (fun y x => (fun x => Classical.choose ⋯) x = y) y x All goals completed! 🐙 inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtypex:X.toSubtypex':X.toSubtypehx:(fun y x => (fun x => Classical.choose ⋯) x = y) y xhx':(fun y x => (fun x => Classical.choose ⋯) x = y) y x'⊢ x = x' inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtypex:X.toSubtypex':X.toSubtypehx:Classical.choose ⋯ = yhx':Classical.choose ⋯ = y⊢ x = x' inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtypex:X.toSubtypex':X.toSubtypehx:Classical.choose ⋯ = Classical.choose ⋯hx':Classical.choose ⋯ = y⊢ x = x' inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtypex:X.toSubtypex':X.toSubtypehx:Classical.choose ⋯ = Classical.choose ⋯hx':Classical.choose ⋯ = y⊢ (fun x => Classical.choose ⋯) x = (fun x => Classical.choose ⋯) x' All goals completed! 🐙 )
theorem Function.inverse_eval {X Y: Set} {f: Function X Y} (h: f.bijective) (y: Y) (x: X) : x = (f.inverse h) y ↔ f x = y := Function.eval _ _ _

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

theorem declaration uses 'sorry'Function.inverse_eq {X Y: Set} [Nonempty X] {f: Function X Y} (h: f.bijective) : (f.inverse h).to_fn = Function.invFun f.to_fn := inst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijective⊢ (f.inverse h).to_fn = Function.invFun f.to_fn All goals completed! 🐙

Вправа 3.3.1

theorem declaration uses 'sorry'Function.refl {X Y:Set} (f: Function X Y) : f = f := inst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f = f All goals completed! 🐙
theorem declaration uses 'sorry'Function.symm {X Y:Set} (f g: Function X Y) : f = g ↔ g = f := inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g ↔ g = f All goals completed! 🐙theorem declaration uses 'sorry'Function.trans {X Y:Set} {f g h: Function X Y} (hfg: f = g) (hgh: g = h) : f = h := inst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:Function X Yhfg:f = ghgh:g = h⊢ f = h All goals completed! 🐙theorem declaration uses 'sorry'Function.comp_congr {X Y Z:Set} {f f': Function X Y} (hff': f = f') {g g': Function Y Z} (hgg': g = g') : g ○ f = g' ○ f' := inst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yf':Function X Yhff':f = f'g:Function Y Zg':Function Y Zhgg':g = g'⊢ g○f = g'○f' All goals completed! 🐙

Вправа 3.3.2

theorem declaration uses 'sorry'Function.comp_of_inj {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 := inst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.one_to_onehg:g.one_to_one⊢ (g○f).one_to_one All goals completed! 🐙
theorem declaration uses 'sorry'Function.comp_of_surj {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hf: f.onto) (hg: g.onto) : (g ○ f).onto := inst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.ontohg:g.onto⊢ (g○f).onto All goals completed! 🐙

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

declaration uses 'sorry'example (X: Set) : (SetTheory.Set.f_3_3_9 X).one_to_one ↔ sorry := inst✝:SetTheoryX:Set⊢ X.f_3_3_9.one_to_one ↔ sorry All goals completed! 🐙
declaration uses 'sorry'example (X: Set) : (SetTheory.Set.f_3_3_9 X).onto ↔ sorry := inst✝:SetTheoryX:Set⊢ X.f_3_3_9.onto ↔ sorry All goals completed! 🐙declaration uses 'sorry'example (X: Set) : (SetTheory.Set.f_3_3_9 X).bijective ↔ sorry := inst✝:SetTheoryX:Set⊢ X.f_3_3_9.bijective ↔ sorry All goals completed! 🐙

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

theorem declaration uses 'sorry'Function.comp_cancel_left {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' := inst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yf':Function X Yg:Function Y Zheq:g○f = g○f'hg:g.one_to_one⊢ f = f' All goals completed! 🐙
theorem declaration uses 'sorry'Function.comp_cancel_right {X Y Z:Set} {f: Function X Y} {g g': Function Y Z} (heq : g ○ f = g' ○ f) (hf: g.onto) : g = g' := inst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zg':Function Y Zheq:g○f = g'○fhf:g.onto⊢ g = g' All goals completed! 🐙

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

theorem declaration uses 'sorry'Function.comp_injective {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hinj : (g ○ f).one_to_one) : f.one_to_one := inst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhinj:(g○f).one_to_one⊢ f.one_to_one All goals completed! 🐙
theorem declaration uses 'sorry'Function.comp_surjective {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hinj : (g ○ f).onto) : g.onto := inst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhinj:(g○f).onto⊢ g.onto All goals completed! 🐙

Вправа 3.3.6

theorem declaration uses 'sorry'Function.inverse_comp_self {X Y: Set} {f: Function X Y} (h: f.bijective) (x: X) : (f.inverse h) (f x) = x := inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex:X.toSubtype⊢ (fun x => Classical.choose ⋯) ((fun x => Classical.choose ⋯) x) = x All goals completed! 🐙
theorem declaration uses 'sorry'Function.self_comp_inverse {X Y: Set} {f: Function X Y} (h: f.bijective) (y: Y) : f ((f.inverse h) y) = y := inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtype⊢ (fun x => Classical.choose ⋯) ((fun x => Classical.choose ⋯) y) = y All goals completed! 🐙theorem declaration uses 'sorry'Function.inverse_bijective {X Y: Set} {f: Function X Y} (h: f.bijective) : (f.inverse h).bijective := inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijective⊢ (f.inverse h).bijective All goals completed! 🐙theorem declaration uses 'sorry'Function.inverse_inverse {X Y: Set} {f: Function X Y} (h: f.bijective) : (f.inverse h).inverse (f.inverse_bijective h) = f := inst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijective⊢ (f.inverse h).inverse ⋯ = f All goals completed! 🐙theorem declaration uses 'sorry'Function.comp_bijective {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hf: f.bijective) (hg: g.bijective) : (g ○ f).bijective := inst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.bijectivehg:g.bijective⊢ (g○f).bijective All goals completed! 🐙

Вправа 3.3.7

theorem declaration uses 'sorry'Function.inv_of_comp {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hf: f.bijective) (hg: g.bijective) : (g ○ f).inverse (Function.comp_bijective hf hg) = (f.inverse hf) ○ (g.inverse hg) := inst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.bijectivehg:g.bijective⊢ (g○f).inverse ⋯ = f.inverse hf○g.inverse hg All goals completed! 🐙

Вправа 3.3.8

abbrev Function.inclusion {X Y:Set} (h: X ⊆ Y) : Function X Y := Function.mk_fn (fun x ↦ ⟨ x.val, h x.val x.property ⟩ )
abbrev Function.id (X:Set) : Function X X := Function.mk_fn (fun x ↦ x)theorem declaration uses 'sorry'Function.inclusion_id (X:Set) : Function.inclusion (SetTheory.Set.subset_self X) = Function.id X := inst✝:SetTheoryX:Set⊢ inclusion ⋯ = id X All goals completed! 🐙theorem declaration uses 'sorry'Function.inclusion_comp (X Y Z:Set) (hXY: X ⊆ Y) (hYZ: Y ⊆ Z) : Function.inclusion hYZ ○ Function.inclusion hXY = Function.inclusion (SetTheory.Set.subset_trans hXY hYZ) := inst✝:SetTheoryX:SetY:SetZ:SethXY:X ⊆ YhYZ:Y ⊆ Z⊢ inclusion hYZ○inclusion hXY = inclusion ⋯ All goals completed! 🐙theorem declaration uses 'sorry'Function.comp_id {A B:Set} (f: Function A B) : f ○ Function.id A = f := inst✝:SetTheoryA:SetB:Setf:Function A B⊢ f○id A = f All goals completed! 🐙theorem declaration uses 'sorry'Function.id_comp {A B:Set} (f: Function A B) : Function.id B ○ f = f := inst✝:SetTheoryA:SetB:Setf:Function A B⊢ id B○f = f All goals completed! 🐙theorem declaration uses 'sorry'Function.comp_inv {A B:Set} (f: Function A B) (hf: f.bijective) : f ○ f.inverse hf = Function.id B := inst✝:SetTheoryA:SetB:Setf:Function A Bhf:f.bijective⊢ f○f.inverse hf = id B All goals completed! 🐙theorem declaration uses 'sorry'Function.inv_comp {A B:Set} (f: Function A B) (hf: f.bijective) : f.inverse hf ○ f = Function.id A := inst✝:SetTheoryA:SetB:Setf:Function A Bhf:f.bijective⊢ f.inverse hf○f = id A All goals completed! 🐙theorem declaration uses 'sorry'Function.glue {X Y Z:Set} (hXY: Disjoint X Y) (f: Function X Z) (g: Function Y Z) : ∃! h: Function (X ∪ Y) Z, (h ○ Function.inclusion (SetTheory.Set.subset_union_left X Y) = f) ∧ (h ○ Function.inclusion (SetTheory.Set.subset_union_right X Y) = g) := inst✝:SetTheoryX:SetY:SetZ:SethXY:Disjoint X Yf:Function X Zg:Function Y Z⊢ ∃! h, h○inclusion ⋯ = f ∧ h○inclusion ⋯ = g All goals completed! 🐙end Chapter3