Analysis I, Section 3.3: Functions

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• A notion of function Function X Y between two sets X, Y in the set theory of Section 3.1
• Various relations with the Mathlib notion of a function X → Y between two types X, Y. (Note from Section 3.1 that every Set X can also be viewed as a subtype {x : Object // x ∈ X } of Object.)
• Basic function properties and operations, such as composition, one-to-one and onto functions, and inverses.

In the rest of the book we will deprecate the Chapter 3 version of a function, and work with the Mathlib notion of a function instead. Even within this section, we will switch to the Mathlib formalism for some of the examples involving number systems such as ℤ or ℝ that have not been implemented in the Chapter 3 framework.

We will work here with the version Nat of the natural numbers internal to the Chapter 3 set theory, though usually we will use coercions to then immediately translate to the Mathlib natural numbers ℕ.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

• (Add tip here)

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

Definition 3.3.1. Function X Y is the structure of functions from X to Y. Analogous to the Mathlib type 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

Converting a Chapter 3 function f: Function X Y to a Mathlib function f: X → Y. The Chapter 3 definition of a function was nonconstructive, so we have to use the axiom of choice here.

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

Converting a Mathlib function to a Chapter 3 Function

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

Definition 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

Example 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

Create a version of a non-zero n inside Nat \ {0} for any natural number 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

Example 3.3.5. The unused variable _x is underscored to avoid triggering a linter.

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

Definition 3.3.8 (Equality of functions)

@[reducible, inline]

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

Example 3.3.10 (simplified). The second part of the example is tricky to replicate in this formalism, so a Mathlib substitute is offered instead.

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

Example 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

Definition 3.3.13 (Composition)

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

Compatibility with Mathlib's composition operation.

@[reducible, inline]

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

Example 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

Lemma 3.3.15 (Composition is associative)

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

Compatibility with Mathlib's Function.Injective. You may wish to use the unfold tactic to understand Mathlib concepts such as 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

Example 3.3.18. One half of the example requires the integers, and so is expressed using Mathlib functions instead of Chapter 3 functions.

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'

Remark 3.3.19

@[reducible, inline]

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

Definition 3.3.20 (Onto functions)

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

Compatibility with Mathlib's 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

Definition 3.3.23 (Bijective functions)

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

Compatibility with Mathlib's Function.Bijective

@[reducible, inline]

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

Example 3.3.24 (using 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

Remark 3.3.27

@[reducible, inline]

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

We cannot use the notation f⁻¹ for the inverse because in Mathlib's Inv class, the inverse of f must be exactly of the same type of f, and Function Y X is a different type from 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

Compatibility with Mathlib's notion of inverse

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

Exercise 3.3.1. Although a proof operating directly on functions would be shorter, the spirit of the exercise is to show these using the Function.eq_iff definition.

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

Exercise 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

Exercise 3.3.3 - fill in the sorrys in the statements in a reasonable fashion.

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'

Exercise 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

Exercise 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

Exercise 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

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

Exercise 3.3.7

@[reducible, inline]

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

Exercise 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