Analysis
3.3. Functions

Imports

import Mathlib.Tactic
import Analysis.Section_3_1
import Analysis.Tools.ExistsUnique

set_option doc.verso.suggestions false

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)

              namespace Chapter3export SetTheory (Set Object)variable [SetTheory]

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

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

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.

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

Converting a Mathlib function to a Chapter 3 Function

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! 🐙)

Definition 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! 🐙

Example 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_existsUniquetheorem 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' 4theorem 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) = xtheorem 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
  -- Some technical unpacking here due to the subtle distinctions between the `Object` type,
  -- sets converted to subtypes of `Object`, and subsets of those sets.
  obtain ⟨ x, hx ⟩ := xinst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}⊢ ∃! y, P_3_3_3c ⟨x, hx⟩ y; simp at hxinst✝:SetTheoryx:Objecthx✝:x ∈ Nat \ {0}hx:x ∈ Nat ∧ ¬x = 0⊢ ∃! y, P_3_3_3c ⟨x, hx⟩ y; obtain ⟨ hx1, hx2 ⟩ := hxinst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Nathx2:¬x = 0⊢ ∃! y, P_3_3_3c ⟨x, hx⟩ y
  set n := ((⟨ x, hx1 ⟩:Nat):ℕ)inst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Nathx2:¬x = 0n:ℕ := nat_equiv.symm ⟨x, hx1⟩⊢ ∃! 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 ⊢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 := byinst✝:SetTheoryx:(Nat \ {0}).toSubtype⊢ ∃! y, P_3_3_3c x y omegaAll goals completed! 🐙
  apply ExistsUnique.intro ((n-1:ℕ):Nat)h₁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 = nh₂inst✝: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)
  .h₁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 simp [←hx2]All goals completed! 🐙
  intro y hyh₂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); 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_existsUniquetheorem 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 _ _ _

Create a version of a non-zero n inside Nat \ {0} for any natural number 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! 🐙/--
  Example 3.3.4 is a little tricky to replicate with the current formalism as the real numbers
  have not been constructed yet.  Instead, I offer some Mathlib counterparts, using the
  Mathlib API for {name}`NNReal` and {lean}`ℝ`.
-/
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⟩ := hinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = x⊢ False; set y := f (-1)inst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = xy:ℝ := f (-1)⊢ False
  have h1 := (hf _ y).mp (byinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = xy:ℝ := f (-1)⊢ y = f ?m.51 rflAll goals completed! 🐙)
  have h2 := sq_nonneg yinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = xy:ℝ := f (-1)h1:y ^ 2 = -1h2:0 ≤ y ^ 2⊢ 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⟩ := hinst✝:SetTheoryf:NNReal → ℝhf:∀ (x : NNReal) (y : ℝ), y = f x ↔ y ^ 2 = ↑x⊢ False; specialize hf 4inst✝:SetTheoryf:NNReal → ℝhf:∀ (y : ℝ), y = f 4 ↔ y ^ 2 = ↑4⊢ False; set y := f 4inst✝:SetTheoryf:NNReal → ℝy:ℝ := f 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4⊢ False
  have hy := (hf y).mp (byinst✝:SetTheoryf:NNReal → ℝy:ℝ := f 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:ℝ := f 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4hy:y ^ 2 = ↑4⊢ 2 ^ 2 = ↑4 norm_numAll goals completed! 🐙)
  have h2 : -2 = y := (hf (-2)).mpr (byinst✝:SetTheoryf:NNReal → ℝy:ℝ := f 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4hy:y ^ 2 = ↑4h1:2 = y⊢ (-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! 🐙

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

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_existsUniquetheorem 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! 🐙

Definition 3.3.8 (Equality of functions)

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

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.

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 [inst✝:SetTheory⊢ f_3_3_10a = f_3_3_10bFunction.eq_iff, Function.eval_of]
  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 [inst✝:SetTheory⊢ (fun x ↦ ↑x) = fun x ↦ |↑x|NNReal.abs_eq]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:ℝ := (fun x ↦ x) (-1)⊢ False
  let b := (fun x:ℝ ↦ |(x:ℝ)|) (-1)inst✝:SetTheoryh:(fun x ↦ x) = fun x ↦ |x|a:ℝ := (fun x ↦ x) (-1)b:ℝ := (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:ℝ := (fun x ↦ x) (-1)b:ℝ := (fun x ↦ |x|) (-1)⊢ (fun x ↦ x) (-1) = b; rw [h]All goals completed! 🐙
  norm_num [a, b] at habAll goals completed! 🐙

Example 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_1 ↦ True) x y intro ⟨ x, hx ⟩inst✝:SetTheoryX:Setx:Objecthx:x ∈ ∅⊢ ∃! y, (fun x x_1 ↦ 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! 🐙

Definition 3.3.13 (Composition)

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))

-- `∘` is already taken in Mathlib for the composition of Mathlib functions,
-- so we use `○` here instead to avoid ambiguity.
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 _ _

Compatibility with Mathlib's composition operation.

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! 🐙

Example 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! 🐙

Lemma 3.3.15 (Composition is associative)

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! 🐙

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

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 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 _ _inst✝:SetTheoryx✝:Nat.toSubtypex'✝: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'✝ 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 = 1h2:(fun n ↦ n ^ 2) (-1) = (fun n ↦ n ^ 2) 1⊢ False
  specialize h h2inst✝:SetTheoryh1:(fun n ↦ n ^ 2) 1 = 1h2:(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₂✝:ℕ⊢ (fun n ↦ n ^ 2) a₁✝ = (fun n ↦ n ^ 2) a₂✝ → a₁✝ = a₂✝ _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

Remark 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! 🐙

Definition 3.3.20 (Onto functions)

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

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

              /-- Example 3.3.21 (using 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⟩⟩inst✝: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! 🐙

Definition 3.3.23 (Bijective functions)

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

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

Example 3.3.24 (using 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! 🐙/--
  Example 3.3.25 is formulated using Mathlib rather than the set theory framework here to avoid
  some tedious technical issues (cf. Exercise 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⊢ ¬Function.Bijective fun n ↦ n + 1 unfold Function.Bijectiveinst✝:SetTheoryh:¬Function.Surjective fun n ↦ n + 1⊢ ¬((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! 🐙

Remark 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:Function ?m.31 Nat := mk_fn fun x ↦ 0⊢ ∃ f, (∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x) ∧ ¬f.bijective; use fhinst✝:SetTheoryf:Function ?m.31 Nat := mk_fn fun x ↦ 0⊢ (∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x) ∧ ¬f.bijective
  constructorh.leftinst✝:SetTheoryf:Function ?m.31 Nat := mk_fn fun x ↦ 0⊢ ∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn xh.rightinst✝:SetTheoryf:Function ?m.31 Nat := mk_fn fun x ↦ 0⊢ ¬f.bijective
  ·h.leftinst✝:SetTheoryf:Function ?m.31 Nat := mk_fn fun x ↦ 0⊢ ∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x introsh.leftinst✝:SetTheoryf:Function ?m.31 Nat := mk_fn fun x ↦ 0x✝:Nat.toSubtype⊢ ∃! y, y = f.to_fn x✝
    apply existsUnique_of_exists_of_uniqueh.left.hexinst✝:SetTheoryf:Function ?m.31 Nat := mk_fn fun x ↦ 0x✝:Nat.toSubtype⊢ ∃ x, x = f.to_fn x✝h.left.huniqueinst✝:SetTheoryf:Function ?m.31 Nat := 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:Function ?m.31 Nat := mk_fn fun x ↦ 0x✝:Nat.toSubtype⊢ ∃ x, x = f.to_fn x✝ use 0hinst✝:SetTheoryf:Function ?m.31 Nat := mk_fn fun x ↦ 0x✝:Nat.toSubtype⊢ 0 = f.to_fn x✝; rw [Function.eval]All goals completed! 🐙
    introsh.left.huniqueinst✝:SetTheoryf:Function ?m.31 Nat := 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:Function ?m.31 Nat := 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:Function ?m.31 Nat := mk_fn fun x ↦ 0⊢ ¬(f.one_to_one ∧ f.onto)
  suffices h : ¬ f.one_to_one byinst✝:SetTheoryf:Function Nat Nat := mk_fn fun x ↦ 0h:¬f.one_to_one⊢ ¬(f.one_to_one ∧ f.onto) tautoAll goals completed! 🐙
  rw [Function.one_to_one_iff]h.rightinst✝:SetTheoryf:Function ?m.31 Nat := mk_fn fun x ↦ 0⊢ ¬∀ (x x' : Nat.toSubtype), f.to_fn x = f.to_fn x' → x = x'
  push_negh.rightinst✝:SetTheoryf:Function ?m.31 Nat := mk_fn fun x ↦ 0⊢ ∃ x x', f.to_fn x = f.to_fn x' ∧ x ≠ x'; use 0, 1hinst✝:SetTheoryf:Function ?m.31 Nat := mk_fn fun x ↦ 0⊢ f.to_fn 0 = f.to_fn 1 ∧ 0 ≠ 1; simp [f]All goals completed! 🐙

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.

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 _ _huniqueinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtypey₁✝:X.toSubtypey₂✝:X.toSubtype⊢ (fun y x ↦ f.to_fn x = y) x✝ y₁✝ → (fun y x ↦ f.to_fn x = y) x✝ y₂✝ → y₁✝ = y₂✝ hxhuniqueinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtypey₁✝:X.toSubtypey₂✝:X.toSubtypehx:(fun y x ↦ f.to_fn x = y) x✝ y₁✝⊢ (fun y x ↦ f.to_fn x = y) x✝ y₂✝ → y₁✝ = y₂✝ 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 _ _ _

Compatibility with Mathlib's notion of inverse

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! 🐙

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 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! 🐙

Exercise 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! 🐙

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

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! 🐙

Exercise 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')
  -- the first line of this construction should be either `apply isTrue` or `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')
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

Exercise 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)
  -- the first line of this construction should be either `apply isTrue` or `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)
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

Exercise 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! 🐙

Exercise 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! 🐙

Exercise 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