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

@[implicit_reducible]

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_1 : 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

Exercise 3.3.7

theorem Chapter3.Function.inv_of_comp [SetTheory] {X Y Z : Set} {f : Function X Y} {g : Function Y Z} (hf : f.bijective) (hg : g.bijective) : (g○f).inverse ⋯ = f.inverse hf○g.inverse hg

@[reducible, inline]

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

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