Функції

Аналіз I, Розділ 3.3: Функції

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

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

Поняття функції Unknown identifier `Function`Function X Y між двома множинами Unknown identifier `X`X, Unknown identifier `Y`Y в теорії множин із глави 3.1
Різні співвідношення з поняттям функції Unknown identifier `X`sorry → sorry : Sort (imax u_1 u_2)X → Unknown identifier `Y`Y у Mathlib між двома типами Unknown identifier `X`X, Unknown identifier `Y`Y. (Примітка із глави 3.1, що кожна Set.{u} (α : Type u) : Type uSet Unknown identifier `X`X також може бути розглянути як підтип { x // x ∈ sorry } : Type u_1{x : Unknown identifier `Object`Object // x ∈ Unknown identifier `X`X } Unknown identifier `Object`Object.)
Основні властивості та операції над функціями, такі як композиція, ін'єктивні функції, сур'єктивні функції, та обернені функції.

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

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

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

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

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

namespace Chapter3export SetTheory (Set Object)variable [SetTheory]

Визначення 3.3.1. Function sorry sorry : Type u_2Function Unknown identifier `X`X Unknown identifier `Y`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.{u_1, u_2} [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 def Function.to_fn {X Y: Set} (f: Function X Y) : X → Y :=
  fun x ↦ (f.unique x).choose

noncomputable instance Function.inst_coefn (X Y: Set) : CoeFun (Function X Y) (fun _ ↦ X → Y) where
  coe := Function.to_fn

theorem Function.to_fn_eval {X Y: Set} (f: Function X Y) (x:X) : f.to_fn x = f x := rfl

Перетворення функції Mathlib на Chapter3.Function.{u_1, u_2} [SetTheory] (X Y : Set) : Type u_2Function з Розділу 3

abbrev Function.mk_fn {X Y: Set} (f: X → Y) : Function X Y :=
  Function.mk (fun x y ↦ y = f x) (byinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtype⊢ ∀ (x : X.toSubtype), ∃! y, (fun x y => y = f x) x y simpAll 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 := byinst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypey:Y.toSubtype⊢ y = f.to_fn x ↔ f.P x y
  convert ((f.unique x).choose_iff y).symmAll goals completed! 🐙

@[simp]
theorem Function.eval_of {X Y: Set} (f: X → Y) (x:X) : (Function.mk_fn f) x = f x := byinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtype⊢ (mk_fn f).to_fn x = f x
  symminst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtype⊢ f x = (mk_fn f).to_fn x; rw [eval]All goals completed! 🐙

Приклад 3.3.3.

abbrev P_3_3_3a : Nat → Nat → Prop := fun x y ↦ (y:ℕ) = (x:ℕ)+1

theorem SetTheory.Set.P_3_3_3a_existsUnique (x: Nat) : ∃! y: Nat, P_3_3_3a x y := byinst✝:SetTheoryx:Nat.toSubtype⊢ ∃! y, P_3_3_3a x y
  apply ExistsUnique.intro ((x+1:ℕ):Nat)h₁inst✝:SetTheoryx:Nat.toSubtype⊢ P_3_3_3a x ↑(nat_equiv.symm x + 1)h₂inst✝:SetTheoryx:Nat.toSubtype⊢ ∀ (y : Nat.toSubtype), P_3_3_3a x y → y = ↑(nat_equiv.symm x + 1)
  .h₁inst✝:SetTheoryx:Nat.toSubtype⊢ P_3_3_3a x ↑(nat_equiv.symm x + 1) simp [P_3_3_3a]All goals completed! 🐙
  intro y hh₂inst✝:SetTheoryx:Nat.toSubtypey:Nat.toSubtypeh:P_3_3_3a x y⊢ y = ↑(nat_equiv.symm x + 1)
  simpa [P_3_3_3a, Equiv.symm_apply_eq] using hAll goals completed! 🐙

abbrev SetTheory.Set.f_3_3_3a : Function Nat Nat := Function.mk P_3_3_3a P_3_3_3a_existsUnique

theorem SetTheory.Set.f_3_3_3a_eval (x y: Nat) : y = f_3_3_3a x ↔ (y:ℕ) = (x+1:ℕ) :=
  Function.eval _ _ _

theorem SetTheory.Set.f_3_3_3a_eval' (n: ℕ) : f_3_3_3a (n:Nat) = (n+1:ℕ) := byinst✝:SetTheoryn:ℕ⊢ f_3_3_3a.to_fn ↑n = ↑(n + 1)
  symminst✝:SetTheoryn:ℕ⊢ ↑(n + 1) = f_3_3_3a.to_fn ↑n
  simp only [f_3_3_3a_eval, nat_equiv_coe_of_coe]All goals completed! 🐙

theorem SetTheory.Set.f_3_3_3a_eval'' : f_3_3_3a 4 = 5 := f_3_3_3a_eval' 4

theorem SetTheory.Set.f_3_3_3a_eval''' (n:ℕ) : f_3_3_3a (2*n+3: ℕ) = (2*n+4:ℕ) := byinst✝:SetTheoryn:ℕ⊢ f_3_3_3a.to_fn ↑(2 * n + 3) = ↑(2 * n + 4)
  convert f_3_3_3a_eval' _All goals completed! 🐙

abbrev SetTheory.Set.P_3_3_3b : Nat → Nat → Prop := fun x y ↦ (y+1:ℕ) = (x:ℕ)

theorem SetTheory.Set.not_P_3_3_3b_existsUnique : ¬ ∀ x, ∃! y: Nat, P_3_3_3b x y := byinst✝:SetTheory⊢ ¬∀ (x : Nat.toSubtype), ∃! y, P_3_3_3b x y
  by_contra hinst✝:SetTheoryh:∀ (x : Nat.toSubtype), ∃! y, P_3_3_3b x y⊢ False
  choose n hn _ using h (0:Nat)inst✝:SetTheoryh:∀ (x : Nat.toSubtype), ∃! y, P_3_3_3b x yn:Nat.toSubtypehn:P_3_3_3b 0 na✝:∀ (y : Nat.toSubtype), (fun y => P_3_3_3b 0 y) y → y = n⊢ False
  have : ((0:Nat):ℕ) = 0 := byinst✝:SetTheory⊢ ¬∀ (x : Nat.toSubtype), ∃! y, P_3_3_3b x y simp [OfNat.ofNat]All goals completed! 🐙
  simp [P_3_3_3b, this] at hnAll goals completed! 🐙

abbrev SetTheory.Set.P_3_3_3c : (Nat \ {(0:Object)}: Set) → Nat → Prop :=
  fun x y ↦ ((y+1:ℕ):Object) = x

theorem SetTheory.Set.P_3_3_3c_existsUnique (x: (Nat \ {(0:Object)}: Set)) :
    ∃! y: Nat, P_3_3_3c x y := byinst✝:SetTheoryx:(Nat \ {0}).toSubtype⊢ ∃! y, P_3_3_3c x y
  -- Тут йде деяке технічне розпакування пов'язане з тонкими відмінностями між типом `Object`,
  -- множинами, перетвореними на підтипи `Object`, та підмножинами цих множин.
  obtain ⟨ x, hx ⟩ := xmkinst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}⊢ ∃! y, P_3_3_3c ⟨x, hx⟩ y; simp at hxmkinst✝:SetTheoryx:Objecthx✝:x ∈ Nat \ {0}hx:x ∈ Nat ∧ ¬x = 0⊢ ∃! y, P_3_3_3c ⟨x, hx✝⟩ y; obtain ⟨ hx1, hx2 ⟩ := hxmk.introinst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Nathx2:¬x = 0⊢ ∃! y, P_3_3_3c ⟨x, hx⟩ y
  set n := ((⟨ x, hx1 ⟩:Nat):ℕ)mk.introinst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Nathx2:¬x = 0n:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩⊢ ∃! y, P_3_3_3c ⟨x, hx⟩ y
  have : x = (n:Nat) := byinst✝:SetTheoryx:(Nat \ {0}).toSubtype⊢ ∃! y, P_3_3_3c x y simp [n]All goals completed! 🐙
  simp [P_3_3_3c, this, Object.ofnat_eq'] at hx2 ⊢mk.introinst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Natn:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩this:_fvar.50161 = ↑↑_fvar.50593 := ?_mvar.51000hx2:¬n = 0⊢ ∃! y, nat_equiv.symm y + 1 = n
  replace hx2 : n = (n-1) + 1 := byinst✝:SetTheoryx:(Nat \ {0}).toSubtype⊢ ∃! y, P_3_3_3c x y omegaAll goals completed! 🐙
  apply ExistsUnique.intro ((n-1:ℕ):Nat)mk.intro.h₁inst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Natn:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩this:_fvar.50161 = ↑↑_fvar.50593 := ?_mvar.51000hx2:_fvar.50593 = _fvar.50593 - 1 + 1 := ?_mvar.59231⊢ nat_equiv.symm ↑(n - 1) + 1 = nmk.intro.h₂inst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Natn:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩this:_fvar.50161 = ↑↑_fvar.50593 := ?_mvar.51000hx2:_fvar.50593 = _fvar.50593 - 1 + 1 := ?_mvar.59231⊢ ∀ (y : Nat.toSubtype), nat_equiv.symm y + 1 = n → y = ↑(n - 1)
  .mk.intro.h₁inst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Natn:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩this:_fvar.50161 = ↑↑_fvar.50593 := ?_mvar.51000hx2:_fvar.50593 = _fvar.50593 - 1 + 1 := ?_mvar.59231⊢ nat_equiv.symm ↑(n - 1) + 1 = n simp [←hx2]All goals completed! 🐙
  intro y hymk.intro.h₂inst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Natn:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩this:_fvar.50161 = ↑↑_fvar.50593 := ?_mvar.51000hx2:_fvar.50593 = _fvar.50593 - 1 + 1 := ?_mvar.59231y:Nat.toSubtypehy:nat_equiv.symm y + 1 = n⊢ y = ↑(n - 1); simp [←hy]All goals completed! 🐙

abbrev SetTheory.Set.f_3_3_3c : Function (Nat \ {(0:Object)}: Set) Nat :=
  Function.mk P_3_3_3c P_3_3_3c_existsUnique

theorem SetTheory.Set.f_3_3_3c_eval (x: (Nat \ {(0:Object)}: Set)) (y: Nat) :
    y = f_3_3_3c x ↔ ((y+1:ℕ):Object) = x := Function.eval _ _ _

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

abbrev SetTheory.Set.coe_nonzero (n:ℕ) (h: n ≠ 0): (Nat \ {(0:Object)}: Set) :=
  ⟨((n:ℕ):Object), byinst✝:SetTheoryn:ℕh:n ≠ 0⊢ ↑n ∈ Nat \ {0}
    simp [Object.ofnat_eq',h]inst✝:SetTheoryn:ℕh:n ≠ 0⊢ ↑n ∈ Nat
    rw [←Object.ofnat_eq]inst✝:SetTheoryn:ℕh:n ≠ 0⊢ ↑↑n ∈ Nat
    exact Subtype.property _All goals completed! 🐙
  ⟩

theorem SetTheory.Set.f_3_3_3c_eval' (n: ℕ) : f_3_3_3c (coe_nonzero (n+1) (byinst✝:SetTheoryn:ℕ⊢ n + 1 ≠ 0 positivityAll goals completed! 🐙)) = n := byinst✝:SetTheoryn:ℕ⊢ f_3_3_3c.to_fn (coe_nonzero (n + 1) ⋯) = ↑n
  symminst✝:SetTheoryn:ℕ⊢ ↑n = f_3_3_3c.to_fn (coe_nonzero (n + 1) ⋯); simp [f_3_3_3c_eval]All goals completed! 🐙

theorem SetTheory.Set.f_3_3_3c_eval'' : f_3_3_3c (coe_nonzero 4 (byinst✝:SetTheory⊢ 4 ≠ 0 positivityAll goals completed! 🐙)) = 3 := byinst✝:SetTheory⊢ f_3_3_3c.to_fn (coe_nonzero 4 ⋯) = 3
  convert f_3_3_3c_eval' 3All goals completed! 🐙

theorem SetTheory.Set.f_3_3_3c_eval''' (n:ℕ) :
    f_3_3_3c (coe_nonzero (2*n+3) (byinst✝:SetTheoryn:ℕ⊢ 2 * n + 3 ≠ 0 positivityAll goals completed! 🐙)) = (2*n+2:ℕ) := byinst✝:SetTheoryn:ℕ⊢ f_3_3_3c.to_fn (coe_nonzero (2 * n + 3) ⋯) = ↑(2 * n + 2) convert f_3_3_3c_eval' (2*n+2)All goals completed! 🐙

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

example : ¬ ∃ f: ℝ → ℝ, ∀ x y, y = f x ↔ y^2 = x := byinst✝:SetTheory⊢ ¬∃ f, ∀ (x y : ℝ), y = f x ↔ y ^ 2 = x
  by_contra hinst✝:SetTheoryh:∃ f, ∀ (x y : ℝ), y = f x ↔ y ^ 2 = x⊢ False
  obtain ⟨f, hf⟩ := hintroinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = x⊢ False; set y := f (-1)introinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = xy:ℝ := @_fvar.81408 (-1)⊢ False
  have h1 := (hf _ y).mp (byinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = xy:ℝ := @_fvar.81408 (-1)⊢ y = f ?m.49 rflAll goals completed! 🐙)
  have h2 := sq_nonneg yintroinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = xy:ℝ := @_fvar.81408 (-1)h1:?_mvar.81525 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h2:?_mvar.81542 := sq_nonneg _fvar.81471⊢ False
  linarithAll goals completed! 🐙

example : ¬ ∃ f: NNReal → ℝ, ∀ x y, y = f x ↔ y^2 = x := byinst✝:SetTheory⊢ ¬∃ f, ∀ (x : NNReal) (y : ℝ), y = f x ↔ y ^ 2 = ↑x
  by_contra hinst✝:SetTheoryh:∃ f, ∀ (x : NNReal) (y : ℝ), y = f x ↔ y ^ 2 = ↑x⊢ False
  obtain ⟨f, hf⟩ := hintroinst✝:SetTheoryf:NNReal → ℝhf:∀ (x : NNReal) (y : ℝ), y = f x ↔ y ^ 2 = ↑x⊢ False; specialize hf 4introinst✝:SetTheoryf:NNReal → ℝhf:∀ (y : ℝ), y = f 4 ↔ y ^ 2 = ↑4⊢ False; set y := f 4introinst✝:SetTheoryf:NNReal → ℝy:ℝ := @_fvar.82895 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4⊢ False
  have hy := (hf y).mp (byinst✝:SetTheoryf:NNReal → ℝy:ℝ := @_fvar.82895 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4⊢ y = y rflAll goals completed! 🐙)
  have h1 : 2 = y := (hf 2).mpr (byinst✝:SetTheoryf:NNReal → ℝy:ℝ := @_fvar.82895 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4hy:_fvar.83076 ^ 2 = ↑4 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ 2 ^ 2 = ↑4 norm_numAll goals completed! 🐙)
  have h2 : -2 = y := (hf (-2)).mpr (byinst✝:SetTheoryf:NNReal → ℝy:ℝ := @_fvar.82895 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4hy:_fvar.83076 ^ 2 = ↑4 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:2 = _fvar.83076 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ (-2) ^ 2 = ↑4 norm_numAll goals completed! 🐙)
  linarithAll goals completed! 🐙

example : ∃ f: NNReal → NNReal, ∀ x y, y = f x ↔ y^2 = x := byinst✝:SetTheory⊢ ∃ f, ∀ (x y : NNReal), y = f x ↔ y ^ 2 = x
  use NNReal.sqrthinst✝:SetTheory⊢ ∀ (x y : NNReal), y = NNReal.sqrt x ↔ y ^ 2 = x; intro x yhinst✝:SetTheoryx:NNRealy:NNReal⊢ y = NNReal.sqrt x ↔ y ^ 2 = x
  constructorh.mpinst✝:SetTheoryx:NNRealy:NNReal⊢ y = NNReal.sqrt x → y ^ 2 = xh.mprinst✝:SetTheoryx:NNRealy:NNReal⊢ y ^ 2 = x → y = NNReal.sqrt x <;>h.mpinst✝:SetTheoryx:NNRealy:NNReal⊢ y = NNReal.sqrt x → y ^ 2 = xh.mprinst✝:SetTheoryx:NNRealy:NNReal⊢ y ^ 2 = x → y = NNReal.sqrt x intro hh.mprinst✝:SetTheoryx:NNRealy:NNRealh:y ^ 2 = x⊢ y = NNReal.sqrt x
  ·h.mpinst✝:SetTheoryx:NNRealy:NNRealh:y = NNReal.sqrt x⊢ y ^ 2 = x rw [h, NNReal.sq_sqrt]All goals completed! 🐙
  ·h.mprinst✝:SetTheoryx:NNRealy:NNRealh:y ^ 2 = x⊢ y = NNReal.sqrt x rw [←h, NNReal.sqrt_sq]All goals completed! 🐙

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

abbrev SetTheory.Set.P_3_3_5 : Nat → Nat → Prop := fun _x y ↦ y = 7

theorem SetTheory.Set.P_3_3_5_existsUnique (x: Nat) : ∃! y: Nat, P_3_3_5 x y := byinst✝:SetTheoryx:Nat.toSubtype⊢ ∃! y, P_3_3_5 x y
  apply ExistsUnique.intro 7h₁inst✝:SetTheoryx:Nat.toSubtype⊢ P_3_3_5 x 7h₂inst✝:SetTheoryx:Nat.toSubtype⊢ ∀ (y : Nat.toSubtype), P_3_3_5 x y → y = 7 <;>h₁inst✝:SetTheoryx:Nat.toSubtype⊢ P_3_3_5 x 7h₂inst✝:SetTheoryx:Nat.toSubtype⊢ ∀ (y : Nat.toSubtype), P_3_3_5 x y → y = 7 simp [P_3_3_5]All goals completed! 🐙

abbrev SetTheory.Set.f_3_3_5 : Function Nat Nat := Function.mk P_3_3_5 P_3_3_5_existsUnique

theorem SetTheory.Set.f_3_3_5_eval (x: Nat) : f_3_3_5 x = 7 := byinst✝:SetTheoryx:Nat.toSubtype⊢ f_3_3_5.to_fn x = 7
  symminst✝:SetTheoryx:Nat.toSubtype⊢ 7 = f_3_3_5.to_fn x; rw [Function.eval]All goals completed! 🐙

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

theorem Function.eq_iff {X Y: Set} (f g: Function X Y) : f = g ↔ ∀ x: X, f x = g x := byinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g ↔ ∀ (x : X.toSubtype), f.to_fn x = g.to_fn x
  constructormpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g → ∀ (x : X.toSubtype), f.to_fn x = g.to_fn xmprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ (∀ (x : X.toSubtype), f.to_fn x = g.to_fn x) → f = g <;>mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g → ∀ (x : X.toSubtype), f.to_fn x = g.to_fn xmprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ (∀ (x : X.toSubtype), f.to_fn x = g.to_fn x) → f = g intro hmprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn x⊢ f = g
  .mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:f = g⊢ ∀ (x : X.toSubtype), f.to_fn x = g.to_fn x simp [h]All goals completed! 🐙
  ext x ympr.P.h.h.ainst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtype⊢ f.P x y ↔ g.P x y; constructormpr.P.h.h.a.mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtype⊢ f.P x y → g.P x ympr.P.h.h.a.mprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtype⊢ g.P x y → f.P x y <;>mpr.P.h.h.a.mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtype⊢ f.P x y → g.P x ympr.P.h.h.a.mprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtype⊢ g.P x y → f.P x y introsmpr.P.h.h.a.mprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtypea✝:g.P x y⊢ f.P x y
  .mpr.P.h.h.a.mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtypea✝:f.P x y⊢ g.P x y rwa [←Function.eval, ←h x, Function.eval]mpr.P.h.h.a.mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtypea✝:f.P x y⊢ f.P x y
  rwa [←Function.eval, h x, Function.eval]mpr.P.h.h.a.mprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtypea✝:g.P x y⊢ g.P x y

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

abbrev SetTheory.Set.f_3_3_10a : Function Nat Nat := Function.mk_fn (fun x ↦ (x^2 + 2*x + 1:ℕ))

abbrev SetTheory.Set.f_3_3_10b : Function Nat Nat := Function.mk_fn (fun x ↦ ((x+1)^2:ℕ))

theorem SetTheory.Set.f_3_3_10_eq : f_3_3_10a = f_3_3_10b := byinst✝:SetTheory⊢ f_3_3_10a = f_3_3_10b
  simp_rw [Function.eq_iff, Function.eval_of]inst✝:SetTheory⊢ ∀ (x : Nat.toSubtype), ↑(nat_equiv.symm x ^ 2 + 2 * nat_equiv.symm x + 1) = ↑((nat_equiv.symm x + 1) ^ 2)
  introsinst✝:SetTheoryx✝:Nat.toSubtype⊢ ↑(nat_equiv.symm x✝ ^ 2 + 2 * nat_equiv.symm x✝ + 1) = ↑((nat_equiv.symm x✝ + 1) ^ 2); simpinst✝:SetTheoryx✝:Nat.toSubtype⊢ nat_equiv.symm x✝ ^ 2 + 2 * nat_equiv.symm x✝ + 1 = (nat_equiv.symm x✝ + 1) ^ 2; ringAll goals completed! 🐙

example : (fun x:NNReal ↦ (x:ℝ)) = (fun x:NNReal ↦ |(x:ℝ)|) := byinst✝:SetTheory⊢ (fun x => ↑x) = fun x => |↑x|
  simp_rw [NNReal.abs_eq]All goals completed! 🐙

example : (fun x:ℝ ↦ (x:ℝ)) ≠ (fun x:ℝ ↦ |(x:ℝ)|) := byinst✝:SetTheory⊢ (fun x => x) ≠ fun x => |x|
  intro hinst✝:SetTheoryh:(fun x => x) = fun x => |x|⊢ False
  let a := (fun (x:ℝ) ↦ x) (-1)inst✝:SetTheoryh:(fun x => x) = fun x => |x|a:?_mvar.91839 := (fun x => x) (-1)⊢ False
  let b := (fun x:ℝ ↦ |(x:ℝ)|) (-1)inst✝:SetTheoryh:(fun x => x) = fun x => |x|a:?_mvar.91839 := (fun x => x) (-1)b:?_mvar.91906 := (fun x => |x|) (-1)⊢ False
  have hab : a = b := byinst✝:SetTheory⊢ (fun x => x) ≠ fun x => |x| unfold ainst✝:SetTheoryh:(fun x => x) = fun x => |x|a:?_mvar.91839 := (fun x => x) (-1)b:?_mvar.91906 := (fun x => |x|) (-1)⊢ (fun x => x) (-1) = b; rw [h]All goals completed! 🐙
  norm_num [a, b] at habAll goals completed! 🐙

Приклад 3.3.11

abbrev SetTheory.Set.f_3_3_11 (X:Set) : Function (∅:Set) X :=
  Function.mk (fun _ _ ↦ True) (byinst✝:SetTheoryX:Set⊢ ∀ (x : ∅.toSubtype), ∃! y, (fun x x => True) x y intro ⟨ x,hx ⟩inst✝:SetTheoryX:Setx:Objecthx:x ∈ ∅⊢ ∃! y, (fun x x => True) ⟨x, hx⟩ y; simp at hxAll goals completed! 🐙)

theorem declaration uses 'sorry'SetTheory.Set.empty_function_unique {X: Set} (f g: Function (∅:Set) X) : f = g := byinst✝:SetTheoryX:Setf:Function ∅ Xg:Function ∅ X⊢ f = g sorryAll goals completed! 🐙

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

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

theorem 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 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 := byinst✝:SetTheoryX:SetY:SetZ:Setg:Function Y Zf:Function X Y⊢ (g○f).to_fn = g.to_fn ∘ f.to_fn
  exth.ainst✝:SetTheoryX:SetY:SetZ:Setg:Function Y Zf:Function X Yx✝:X.toSubtype⊢ ↑((g○f).to_fn x✝) = ↑((g.to_fn ∘ f.to_fn) x✝); simp only [Function.comp_eval, Function.comp_apply]All goals completed! 🐙

Приклад 3.3.14

abbrev SetTheory.Set.f_3_3_14 : Function Nat Nat := Function.mk_fn (fun x ↦ (2*x:ℕ))

abbrev SetTheory.Set.g_3_3_14 : Function Nat Nat := Function.mk_fn (fun x ↦ (x+3:ℕ))

theorem SetTheory.Set.g_circ_f_3_3_14 :
    g_3_3_14 ○ f_3_3_14 = Function.mk_fn (fun x ↦ ((2*(x:ℕ)+3:ℕ):Nat)) := byinst✝:SetTheory⊢ g_3_3_14○f_3_3_14 = Function.mk_fn fun x => ↑(2 * nat_equiv.symm x + 3)
  simp [Function.eq_iff, Function.eval_of]All goals completed! 🐙

theorem SetTheory.Set.f_circ_g_3_3_14 :
    f_3_3_14 ○ g_3_3_14 = Function.mk_fn (fun x ↦ ((2*(x:ℕ)+6:ℕ):Nat)) := byinst✝:SetTheory⊢ f_3_3_14○g_3_3_14 = Function.mk_fn fun x => ↑(2 * nat_equiv.symm x + 6)
  simp [Function.eq_iff, Function.eval_of]inst✝:SetTheory⊢ ∀ (a : Object) (b : a ∈ Nat), 2 * (nat_equiv.symm ⟨a, b⟩ + 3) = 2 * nat_equiv.symm ⟨a, b⟩ + 6
  introsinst✝:SetTheorya✝:Objectb✝:a✝ ∈ Nat⊢ 2 * (nat_equiv.symm ⟨a✝, b✝⟩ + 3) = 2 * nat_equiv.symm ⟨a✝, b✝⟩ + 6; ringAll goals completed! 🐙

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

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 := byinst✝:SetTheoryW:SetX:SetY:SetZ:Seth:Function Y Zg:Function X Yf:Function W X⊢ h○(g○f) = (h○g)○f
  simp [Function.eq_iff]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' := byinst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.one_to_one ↔ ∀ (x x' : X.toSubtype), f.to_fn x = f.to_fn x' → x = x'
  peel with x hxh.hinst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypehx:X.toSubtype⊢ x ≠ hx → f.to_fn x ≠ f.to_fn hx ↔ f.to_fn x = f.to_fn hx → x = hx; tautoAll 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 Function.one_to_one_iff' {X Y: Set} (f: Function X Y) :
    f.one_to_one ↔ Function.Injective f.to_fn := byinst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.one_to_one ↔ Function.Injective f.to_fn
  rw [one_to_one_iff, Function.Injective]All goals completed! 🐙

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

theorem SetTheory.Set.f_3_3_18_one_to_one :
    (Function.mk_fn (fun (n:Nat) ↦ ((n^2:ℕ):Nat))).one_to_one := byinst✝:SetTheory⊢ (Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).one_to_one
  rw [Function.one_to_one_iff]inst✝:SetTheory⊢ ∀ (x x' : Nat.toSubtype),
  (Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).to_fn x =
      (Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).to_fn x' →
    x = x'
  intro _ _ hinst✝:SetTheoryx✝:Nat.toSubtypex'✝:Nat.toSubtypeh:(Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).to_fn x✝ = (Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).to_fn x'✝⊢ x✝ = x'✝
  simpa [Function.eval, Function.eval_of] using hAll goals completed! 🐙

example : ¬ Function.Injective (fun (n:ℤ) ↦ n^2) := byinst✝:SetTheory⊢ ¬Function.Injective fun n => n ^ 2
  intro hinst✝:SetTheoryh:Function.Injective fun n => n ^ 2⊢ False
  have h1 : (fun n ↦ n ^ 2) 1 = (1:ℤ) := byinst✝:SetTheory⊢ ¬Function.Injective fun n => n ^ 2 norm_numAll goals completed! 🐙
  have h2 : (fun n ↦ n ^ 2) (-1) = (1:ℤ) := byinst✝:SetTheory⊢ ¬Function.Injective fun n => n ^ 2 norm_numAll goals completed! 🐙
  nth_rewrite 2 [←h1] at h2inst✝:SetTheoryh:Function.Injective fun n => n ^ 2h1:(fun n => n ^ 2) 1 = 1 := ?_mvar.127345h2:(fun n => n ^ 2) (-1) = (fun n => n ^ 2) 1⊢ False
  specialize h h2inst✝:SetTheoryh1:(fun n => n ^ 2) 1 = 1 := ?_mvar.127345h2:(fun n => n ^ 2) (-1) = (fun n => n ^ 2) 1h:-1 = 1⊢ False
  contradictionAll goals completed! 🐙

example : Function.Injective (fun (n:ℕ) ↦ n^2) := byinst✝:SetTheory⊢ Function.Injective fun n => n ^ 2
  intro _ _ _inst✝:SetTheorya₁✝:ℕa₂✝:ℕa✝:(fun n => n ^ 2) a₁✝ = (fun n => n ^ 2) a₂✝⊢ a₁✝ = a₂✝; rwa [← pow_left_inj₀ (byinst✝:SetTheorya₁✝:ℕa₂✝:ℕa✝:(fun n => n ^ 2) a₁✝ = (fun n => n ^ 2) a₂✝⊢ 0 ≤ a₁✝ norm_numAll goals completed! 🐙) (byinst✝:SetTheorya₁✝:ℕa₂✝:ℕa✝:(fun n => n ^ 2) a₁✝ = (fun n => n ^ 2) a₂✝⊢ 0 ≤ a₂✝ norm_numAll goals completed! 🐙) (show 2 ≠ 0 byinst✝:SetTheory⊢ Function.Injective fun n => n ^ 2 norm_numAll goals completed! 🐙)]inst✝:SetTheorya₁✝:ℕa₂✝:ℕa✝:(fun n => n ^ 2) a₁✝ = (fun n => n ^ 2) a₂✝⊢ a₁✝ ^ 2 = a₂✝ ^ 2

Ремарка 3.3.19

theorem 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' := byinst✝:SetTheoryX:SetY:Setf:Function X Yh:¬f.one_to_one⊢ ∃ x x', x ≠ x' ∧ f.to_fn x = f.to_fn x'
  rw [Function.one_to_one] at hinst✝:SetTheoryX:SetY:Setf:Function X Yh:¬∀ (x x' : X.toSubtype), x ≠ x' → f.to_fn x ≠ f.to_fn x'⊢ ∃ x x', x ≠ x' ∧ f.to_fn x = f.to_fn x'; aesopAll goals completed! 🐙

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

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

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

theorem Function.onto_iff {X Y: Set} (f: Function X Y) : f.onto ↔ Function.Surjective f.to_fn := byinst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.onto ↔ Function.Surjective f.to_fn rflAll goals completed! 🐙

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

example : ¬ Function.Surjective (fun (n:ℤ) ↦ n^2) := byinst✝:SetTheory⊢ ¬Function.Surjective fun n => n ^ 2
  unfold Function.Surjectiveinst✝:SetTheory⊢ ¬∀ (b : ℤ), ∃ a, (fun n => n ^ 2) a = b; push_neginst✝:SetTheory⊢ ∃ b, ∀ (a : ℤ), a ^ 2 ≠ b
  use (-1)hinst✝:SetTheory⊢ ∀ (a : ℤ), a ^ 2 ≠ -1; intro ahinst✝:SetTheorya:ℤ⊢ a ^ 2 ≠ -1
  linarith [sq_nonneg a]All goals completed! 🐙

abbrev A_3_3_21 := { m:ℤ // ∃ n:ℤ, m = n^2 }

example : Function.Surjective (fun (n:ℤ) ↦ ⟨ n^2, byinst✝:SetTheoryn:ℤ⊢ ∃ n_1, n ^ 2 = n_1 ^ 2 use nAll goals completed! 🐙 ⟩ : ℤ → A_3_3_21) := byinst✝:SetTheory⊢ Function.Surjective fun n => ⟨n ^ 2, ⋯⟩
  rintro ⟨b, ⟨a, ha⟩⟩mk.introinst✝:SetTheoryb:ℤa:ℤha:b = a ^ 2⊢ ∃ a_1, (fun n => ⟨n ^ 2, ⋯⟩) a_1 = ⟨b, ⋯⟩; use ahinst✝:SetTheoryb:ℤa:ℤha:b = a ^ 2⊢ (fun n => ⟨n ^ 2, ⋯⟩) a = ⟨b, ⋯⟩
  simp only [ha]All goals completed! 🐙

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

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

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

theorem Function.bijective_iff {X Y: Set} (f: Function X Y) :
    f.bijective ↔ Function.Bijective f.to_fn := byinst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.bijective ↔ Function.Bijective f.to_fn
  rw [Function.bijective, Function.Bijective, one_to_one_iff', onto_iff]All goals completed! 🐙

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

abbrev f_3_3_24 : Fin 3 → ({3,4}:_root_.Set ℕ) := fun x ↦ match x with
| 0 => ⟨ 3, byinst✝:SetTheoryx:Fin 3⊢ 3 ∈ {3, 4} norm_numAll goals completed! 🐙 ⟩
| 1 => ⟨ 3, byinst✝:SetTheoryx:Fin 3⊢ 3 ∈ {3, 4} norm_numAll goals completed! 🐙 ⟩
| 2 => ⟨ 4, byinst✝:SetTheoryx:Fin 3⊢ 4 ∈ {3, 4} norm_numAll goals completed! 🐙 ⟩

example : ¬ Function.Injective f_3_3_24 := byinst✝:SetTheory⊢ ¬Function.Injective f_3_3_24 decideAll goals completed! 🐙

example : ¬ Function.Bijective f_3_3_24 := byinst✝:SetTheory⊢ ¬Function.Bijective f_3_3_24 decideAll goals completed! 🐙

abbrev g_3_3_24 : Fin 2 → ({2,3,4}:_root_.Set ℕ) := fun x ↦ match x with
| 0 => ⟨ 2, byinst✝:SetTheoryx:Fin 2⊢ 2 ∈ {2, 3, 4} norm_numAll goals completed! 🐙 ⟩
| 1 => ⟨ 3, byinst✝:SetTheoryx:Fin 2⊢ 3 ∈ {2, 3, 4} norm_numAll goals completed! 🐙 ⟩

example : ¬ Function.Surjective g_3_3_24 := byinst✝:SetTheory⊢ ¬Function.Surjective g_3_3_24 decideAll goals completed! 🐙

example : ¬ Function.Bijective g_3_3_24 := byinst✝:SetTheory⊢ ¬Function.Bijective g_3_3_24 decideAll goals completed! 🐙

abbrev h_3_3_24 : Fin 3 → ({3,4,5}:_root_.Set ℕ) := fun x ↦ match x with
| 0 => ⟨ 3, byinst✝:SetTheoryx:Fin 3⊢ 3 ∈ {3, 4, 5} norm_numAll goals completed! 🐙 ⟩
| 1 => ⟨ 4, byinst✝:SetTheoryx:Fin 3⊢ 4 ∈ {3, 4, 5} norm_numAll goals completed! 🐙 ⟩
| 2 => ⟨ 5, byinst✝:SetTheoryx:Fin 3⊢ 5 ∈ {3, 4, 5} norm_numAll goals completed! 🐙 ⟩

example : Function.Bijective h_3_3_24 := byinst✝:SetTheory⊢ Function.Bijective h_3_3_24 decideAll goals completed! 🐙

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

example : Function.Bijective (fun n ↦ ⟨ n+1, byinst✝:SetTheoryn:ℕ⊢ n + 1 ≠ 0 omegaAll goals completed! 🐙⟩ : ℕ → { n:ℕ // n ≠ 0 }) := byinst✝:SetTheory⊢ Function.Bijective fun n => ⟨n + 1, ⋯⟩
  constructorleftinst✝:SetTheory⊢ Function.Injective fun n => ⟨n + 1, ⋯⟩rightinst✝:SetTheory⊢ Function.Surjective fun n => ⟨n + 1, ⋯⟩
  ·leftinst✝:SetTheory⊢ Function.Injective fun n => ⟨n + 1, ⋯⟩ intro _ _leftinst✝:SetTheorya₁✝:ℕa₂✝:ℕ⊢ (fun n => ⟨n + 1, ⋯⟩) a₁✝ = (fun n => ⟨n + 1, ⋯⟩) a₂✝ → a₁✝ = a₂✝
    simp only [Subtype.mk.injEq]leftinst✝:SetTheorya₁✝:ℕa₂✝:ℕ⊢ a₁✝ + 1 = a₂✝ + 1 → a₁✝ = a₂✝; omegaAll goals completed! 🐙
  intro ⟨x, hx⟩rightinst✝:SetTheoryx:ℕhx:x ≠ 0⊢ ∃ a, (fun n => ⟨n + 1, ⋯⟩) a = ⟨x, hx⟩; use x-1hinst✝:SetTheoryx:ℕhx:x ≠ 0⊢ (fun n => ⟨n + 1, ⋯⟩) (x - 1) = ⟨x, hx⟩
  simp only [Subtype.mk.injEq]hinst✝:SetTheoryx:ℕhx:x ≠ 0⊢ x - 1 + 1 = x; omegaAll goals completed! 🐙

example : ¬ Function.Bijective (fun n ↦ n+1) := byinst✝:SetTheory⊢ ¬Function.Bijective fun n => n + 1
  suffices h : ¬ Function.Surjective (fun n ↦ n+1) byinst✝:SetTheoryh:¬Function.Surjective fun n => n + 1 := ?_mvar.230004⊢ ¬Function.Bijective fun n => n + 1 unfold Function.Bijectiveinst✝:SetTheoryh:¬Function.Surjective fun n => n + 1 := ?_mvar.230004⊢ ¬((Function.Injective fun n => n + 1) ∧ Function.Surjective fun n => n + 1); tautoAll goals completed! 🐙
  unfold Function.Surjectiveinst✝:SetTheory⊢ ¬∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b; push_neginst✝:SetTheory⊢ ∃ b, ∀ (a : ℕ), a + 1 ≠ b
  use 0hinst✝:SetTheory⊢ ∀ (a : ℕ), a + 1 ≠ 0; introshinst✝:SetTheorya✝:ℕ⊢ a✝ + 1 ≠ 0
  symmhinst✝:SetTheorya✝:ℕ⊢ 0 ≠ a✝ + 1; apply Nat.zero_ne_add_oneAll goals completed! 🐙

Ремарка 3.3.27

theorem Function.bijective_incorrect_def :
    ∃ X Y: Set, ∃ f: Function X Y, (∀ x: X, ∃! y: Y, y = f x) ∧ ¬ f.bijective := byinst✝:SetTheory⊢ ∃ X Y f, (∀ (x : X.toSubtype), ∃! y, y = f.to_fn x) ∧ ¬f.bijective
  use Nat, Nathinst✝:SetTheory⊢ ∃ f, (∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x) ∧ ¬f.bijective
  set f := mk_fn fun x ↦ (0: Nat)hinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ∃ f, (∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x) ∧ ¬f.bijective; use fhinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ (∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x) ∧ ¬f.bijective
  constructorh.leftinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn xh.rightinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ¬f.bijective
  ·h.leftinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x introsh.leftinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtype⊢ ∃! y, y = f.to_fn x✝
    apply existsUnique_of_exists_of_uniqueh.left.hexinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtype⊢ ∃ x, x = f.to_fn x✝h.left.huniqueinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtype⊢ ∀ (y₁ y₂ : Nat.toSubtype), y₁ = f.to_fn x✝ → y₂ = f.to_fn x✝ → y₁ = y₂
    ·h.left.hexinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtype⊢ ∃ x, x = f.to_fn x✝ use 0hinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtype⊢ 0 = f.to_fn x✝; rw [Function.eval]All goals completed! 🐙
    introsh.left.huniqueinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtypey₁✝:Nat.toSubtypey₂✝:Nat.toSubtypea✝¹:y₁✝ = f.to_fn x✝a✝:y₂✝ = f.to_fn x✝⊢ y₁✝ = y₂✝; rw [Function.eval] at *h.left.huniqueinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtypey₁✝:Nat.toSubtypey₂✝:Nat.toSubtypea✝¹:f.P x✝ y₁✝a✝:f.P x✝ y₂✝⊢ y₁✝ = y₂✝; aesopAll goals completed! 🐙
  rw [Function.bijective]h.rightinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ¬(f.one_to_one ∧ f.onto)
  suffices h : ¬ f.one_to_one byinst✝:SetTheoryf:Chapter3.Function (@Chapter3.Nat _fvar.230652) (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0h:¬Chapter3.Function.one_to_one _fvar.230889 := ?_mvar.231550⊢ ¬(f.one_to_one ∧ f.onto) tautoAll goals completed! 🐙
  rw [Function.one_to_one_iff]h.rightinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ¬∀ (x x' : Nat.toSubtype), f.to_fn x = f.to_fn x' → x = x'
  push_negh.rightinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ∃ x x', f.to_fn x = f.to_fn x' ∧ x ≠ x'; use 0, 1hinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ f.to_fn 0 = f.to_fn 1 ∧ 0 ≠ 1; simp [f]All goals completed! 🐙

Ми не можемо використовувати позначення Unknown identifier `f`sorry⁻¹ : ?m.1f⁻¹ для оберненої функції, оскільки в класі Inv.{u} (α : Type u) : Type uInv Mathlib-у обернена функція Unknown identifier `f`f повинна бути точно такого ж типу, як Unknown identifier `f`f, а Function sorry sorry : Type u_2Function Unknown identifier `Y`Y Unknown identifier `X`X має інший тип, ніж Function sorry sorry : Type u_2Function Unknown identifier `X`X Unknown identifier `Y`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) (byinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijective⊢ ∀ (x : Y.toSubtype), ∃! y, (fun y x => f.to_fn x = y) x y
    introsinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtype⊢ ∃! y, (fun y x => f.to_fn x = y) x✝ y
    apply existsUnique_of_exists_of_uniquehexinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtype⊢ ∃ x, (fun y x => f.to_fn x = y) x✝ xhuniqueinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtype⊢ ∀ (y₁ y₂ : X.toSubtype), (fun y x => f.to_fn x = y) x✝ y₁ → (fun y x => f.to_fn x = y) x✝ y₂ → y₁ = y₂
    .hexinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtype⊢ ∃ x, (fun y x => f.to_fn x = y) x✝ x aesopAll goals completed! 🐙
    intro _ _ hx hx'huniqueinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtypey₁✝:X.toSubtypey₂✝:X.toSubtypehx:(fun y x => f.to_fn x = y) x✝ y₁✝hx':(fun y x => f.to_fn x = y) x✝ y₂✝⊢ y₁✝ = y₂✝; simp at hx hx'huniqueinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtypey₁✝:X.toSubtypey₂✝:X.toSubtypehx:f.to_fn y₁✝ = x✝hx':f.to_fn y₂✝ = x✝⊢ y₁✝ = y₂✝
    rw [←hx'] at hxhuniqueinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtypey₁✝:X.toSubtypey₂✝:X.toSubtypehx:f.to_fn y₁✝ = f.to_fn y₂✝hx':f.to_fn y₂✝ = x✝⊢ y₁✝ = y₂✝
    apply f.one_to_one_iff.mp h.1hunique.ainst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtypey₁✝:X.toSubtypey₂✝:X.toSubtypehx:f.to_fn y₁✝ = f.to_fn y₂✝hx':f.to_fn y₂✝ = x✝⊢ f.to_fn y₁✝ = f.to_fn y₂✝
    simp [hx]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 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 := byinst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijective⊢ (f.inverse h).to_fn = Function.invFun f.to_fn
  ext yh.ainst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijectivey:Y.toSubtype⊢ ↑((f.inverse h).to_fn y) = ↑(Function.invFun f.to_fn y); congrh.a.e_selfinst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijectivey:Y.toSubtype⊢ (f.inverse h).to_fn y = Function.invFun f.to_fn y; symmh.a.e_selfinst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijectivey:Y.toSubtype⊢ Function.invFun f.to_fn y = (f.inverse h).to_fn y
  rw [inverse_eval]h.a.e_selfinst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijectivey:Y.toSubtype⊢ f.to_fn (Function.invFun f.to_fn y) = y
  apply Function.rightInverse_invFun (f.bijective_iff.mp h).2All goals completed! 🐙

Вправа 3.3.1. Хоча доведення, що безпосередньо оперує функціями, було б коротшим, суть вправи полягає в тому, щоб показати це, використовуючи визначення Chapter3.Function.eq_iff.{u_1, u_2} [SetTheory] {X Y : Set} (f g : Function X Y) : f = g ↔ ∀ (x : X.toSubtype), f.to_fn x = g.to_fn xFunction.eq_iff.

theorem declaration uses 'sorry'Function.refl {X Y:Set} (f: Function X Y) : f = f := byinst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f = f sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.symm {X Y:Set} (f g: Function X Y) : f = g ↔ g = f := byinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g ↔ g = f sorryAll 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 := byinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:Function X Yhfg:f = ghgh:g = h⊢ f = h sorryAll 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' := byinst✝: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' sorryAll 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 := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.one_to_onehg:g.one_to_one⊢ (g○f).one_to_one sorryAll 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 := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.ontohg:g.onto⊢ (g○f).onto sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'empty_function_one_to_one_iff (X: Set) (f: Function ∅ X) : f.one_to_one ↔ sorry := byinst✝:SetTheoryX:Setf:Function ∅ X⊢ f.one_to_one ↔ sorry sorryAll goals completed! 🐙

theorem declaration uses 'sorry'empty_function_onto_iff (X: Set) (f: Function ∅ X) : f.onto ↔ sorry := byinst✝:SetTheoryX:Setf:Function ∅ X⊢ f.onto ↔ sorry sorryAll goals completed! 🐙

theorem declaration uses 'sorry'empty_function_bijective_iff (X: Set) (f: Function ∅ X) : f.bijective ↔ sorry:= byinst✝:SetTheoryX:Setf:Function ∅ X⊢ f.bijective ↔ sorry sorryAll goals completed! 🐙

Вправа 3.3.4.

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' := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yf':Function X Yg:Function Y Zheq:g○f = g○f'hg:g.one_to_one⊢ f = f' sorryAll 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: f.onto) : g = g' := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zg':Function Y Zheq:g○f = g'○fhf:f.onto⊢ g = g' sorryAll goals completed! 🐙

def declaration uses 'sorry'Function.comp_cancel_left_without_hg : Decidable (∀ (X Y Z:Set) (f f': Function X Y) (g : Function Y Z) (heq : g ○ f = g ○ f'), f = f') := byinst✝:SetTheory⊢ Decidable (∀ (X Y Z : Set) (f f' : Function X Y) (g : Function Y Z), g○f = g○f' → f = f')
  -- перший рядок цієї побудови має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll goals completed! 🐙

def declaration uses 'sorry'Function.comp_cancel_right_without_hg : Decidable (∀ (X Y Z:Set) (f: Function X Y) (g g': Function Y Z) (heq : g ○ f = g' ○ f), g = g') := byinst✝:SetTheory⊢ Decidable (∀ (X Y Z : Set) (f : Function X Y) (g g' : Function Y Z), g○f = g'○f → g = g')
  -- перший рядок цієї побудови має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll goals completed! 🐙

Вправа 3.3.5.

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 := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhinj:(g○f).one_to_one⊢ f.one_to_one sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.comp_surjective {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hsurj :
    (g ○ f).onto) : g.onto := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhsurj:(g○f).onto⊢ g.onto sorryAll goals completed! 🐙

def declaration uses 'sorry'Function.comp_injective' : Decidable (∀ (X Y Z:Set) (f: Function X Y) (g : Function Y Z) (hinj :
    (g ○ f).one_to_one), g.one_to_one) := byinst✝:SetTheory⊢ Decidable (∀ (X Y Z : Set) (f : Function X Y) (g : Function Y Z), (g○f).one_to_one → g.one_to_one)
  -- перший рядок цієї побудови має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll goals completed! 🐙

def declaration uses 'sorry'Function.comp_surjective' : Decidable (∀ (X Y Z:Set) (f: Function X Y) (g : Function Y Z) (hsurj :
    (g ○ f).onto), f.onto) := byinst✝:SetTheory⊢ Decidable (∀ (X Y Z : Set) (f : Function X Y) (g : Function Y Z), (g○f).onto → f.onto)
  -- перший рядок цієї побудови має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll 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 := byinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex:X.toSubtype⊢ (f.inverse h).to_fn (f.to_fn x) = x sorryAll 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 := byinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtype⊢ f.to_fn ((f.inverse h).to_fn y) = y sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.inverse_bijective {X Y: Set} {f: Function X Y} (h: f.bijective) :
    (f.inverse h).bijective := byinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijective⊢ (f.inverse h).bijective sorryAll 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 := byinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijective⊢ (f.inverse h).inverse ⋯ = f sorryAll goals completed! 🐙

Вправа 3.3.7

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 := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.bijectivehg:g.bijective⊢ (g○f).bijective sorryAll goals completed! 🐙

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) := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.bijectivehg:g.bijective⊢ (g○f).inverse ⋯ = f.inverse hf○g.inverse hg sorryAll 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 := byinst✝:SetTheoryX:Set⊢ inclusion ⋯ = id X sorryAll 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) := byinst✝:SetTheoryX:SetY:SetZ:SethXY:X ⊆ YhYZ:Y ⊆ Z⊢ inclusion hYZ○inclusion hXY = inclusion ⋯ sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.comp_id {A B:Set} (f: Function A B) : f ○ Function.id A = f := byinst✝:SetTheoryA:SetB:Setf:Function A B⊢ f○id A = f sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.id_comp {A B:Set} (f: Function A B) : Function.id B ○ f = f := byinst✝:SetTheoryA:SetB:Setf:Function A B⊢ id B○f = f sorryAll 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 := byinst✝:SetTheoryA:SetB:Setf:Function A Bhf:f.bijective⊢ f○f.inverse hf = id B sorryAll 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 := byinst✝:SetTheoryA:SetB:Setf:Function A Bhf:f.bijective⊢ f.inverse hf○f = id A sorryAll goals completed! 🐙

open Classical in
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) := byinst✝:SetTheoryX:SetY:SetZ:SethXY:Disjoint X Yf:Function X Zg:Function Y Z⊢ ∃! h, h○inclusion ⋯ = f ∧ h○inclusion ⋯ = g sorryAll goals completed! 🐙

open Classical in
theorem declaration uses 'sorry'Function.glue' {X Y Z:Set} (f: Function X Z) (g: Function Y Z)
    (hfg : ∀ x : ((X ∩ Y): Set), f ⟨x.val, byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Zg:Function Y Zx:(X ∩ Y).toSubtype⊢ ↑x ∈ X aesopAll goals completed! 🐙⟩ = g ⟨x.val, byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Zg:Function Y Zx:(X ∩ Y).toSubtype⊢ ↑x ∈ Y aesopAll goals completed! 🐙⟩)  :
    ∃! 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) := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Zg:Function Y Zhfg:∀ (x : (X ∩ Y).toSubtype), f.to_fn ⟨↑x, ⋯⟩ = g.to_fn ⟨↑x, ⋯⟩⊢ ∃! h, h○inclusion ⋯ = f ∧ h○inclusion ⋯ = g sorryAll goals completed! 🐙

end Chapter3