@[reducible, inline]

abbrev cartesianProductElementCollection {α : Type u} {β : Type v} (A : Set α) (B : Set β) : Set (α × β)

Definition 0.3.10: For sets A and B, the Cartesian product is the set of ordered pairs (x, y) with x ∈ A and y ∈ B, written A × B.

Equations

• cartesianProductElementCollection A B = A ×ˢ B

theorem cartesianProductElementCollection_eq {α : Type u} {β : Type v} (A : Set α) (B : Set β) : cartesianProductElementCollection A B = A ×ˢ B

The book's Cartesian product coincides with mathlib's set product.

theorem mem_cartesianProductElementCollection {α : Type u} {β : Type v} {A : Set α} {B : Set β} {x : α} {y : β} : (x, y) ∈ cartesianProductElementCollection A B ↔ x ∈ A ∧ y ∈ B

def IsFunctionGraph {α : Type u} {β : Type v} (f : Set (α × β)) (A : Set α) (B : Set β) : Prop

Definition 0.3.11: A function f : A → B is a subset of A × B sending each element of A to a unique y ∈ B; this subset is called the graph of the function. The set A is the domain, R(f) = { y ∈ B | ∃ x ∈ A, (x, y) ∈ f } is the range, and B is the codomain.

Equations

• IsFunctionGraph f A B = ((∀ x ∈ A, ∃! y : β, (x, y) ∈ f) ∧ f ⊆ A ×ˢ B)

def functionGraphRange {α : Type u} {β : Type v} (f : Set (α × β)) (A : Set α) : Set β

The range of a relation f viewed as the graph of a function with domain A.

Equations

• functionGraphRange f A = {y : β | ∃ x ∈ A, (x, y) ∈ f}

noncomputable def functionGraphToSubtypeFun {α : Type u} {β : Type v} (f : Set (α × β)) (A : Set α) (B : Set β) (hf : IsFunctionGraph f A B) : { x : α // x ∈ A } → ↑B

Helper: from a functional graph, choose the output in B for each x ∈ A.

Equations

• functionGraphToSubtypeFun f A B hf x = ⟨Classical.choose ⋯, ⋯⟩

theorem functionGraphToSubtypeFun_mem {α : Type u} {β : Type v} (f : Set (α × β)) (A : Set α) (B : Set β) (hf : IsFunctionGraph f A B) (x : { x : α // x ∈ A }) : (↑x, ↑(functionGraphToSubtypeFun f A B hf x)) ∈ f

Helper: the chosen value from a functional graph lies in the graph.

theorem functionGraphToSubtypeFun_eq_of_mem {α : Type u} {β : Type v} (f : Set (α × β)) (A : Set α) (B : Set β) (hf : IsFunctionGraph f A B) (x : { x : α // x ∈ A }) {y : β} (hy : (↑x, y) ∈ f) : y = ↑(functionGraphToSubtypeFun f A B hf x)

Helper: uniqueness for the chosen value from a functional graph.

def subtypeFunGraph {α : Type u} {β : Type v} (A : Set α) (B : Set β) (g : { x : α // x ∈ A } → ↑B) : Set (α × β)

Helper: the graph set associated to a subtype-valued function.

Equations

• subtypeFunGraph A B g = Set.range fun (x : { x : α // x ∈ A }) => (↑x, ↑(g x))

theorem subtypeFunGraph_isFunctionGraph {α : Type u} {β : Type v} (A : Set α) (B : Set β) (g : { x : α // x ∈ A } → ↑B) : IsFunctionGraph (subtypeFunGraph A B g) A B

Helper: the graph of a subtype-valued function is functional with domain A.

noncomputable def isFunctionGraph_equiv_subtype {α : Type u} {β : Type v} (A : Set α) (B : Set β) : { f : Set (α × β) // IsFunctionGraph f A B } ≃ ({ x : α // x ∈ A } → ↑B)

The book's notion of a functional subset of A × B is equivalent to an ordinary mathlib function with domain the subtype of A and codomain B.

Equations

• One or more equations did not get rendered due to their size.

theorem exists_const_derivative_space : ∃ (_F : { f : ℝ → ℝ // Differentiable ℝ f } → ℝ → ℝ), True

Helper: pick a constant function in the derivative-function space.

theorem exists_const_laplace_space : ∃ (_L : (ℝ → ℝ) → ℝ → ℝ), True

Helper: pick a constant function in the Laplace-transform space.

theorem exists_const_integral_space : ∃ (_I : { g : ℝ → ℝ // ContinuousOn g (Set.Icc 0 1) } → ℝ), True

Helper: pick a constant function in the integral-assigning space.

theorem calculus_function_space_examples : (∃ (_F : { f : ℝ → ℝ // Differentiable ℝ f } → ℝ → ℝ), True) ∧ (∃ (_L : (ℝ → ℝ) → ℝ → ℝ), True) ∧ ∃ (_I : { g : ℝ → ℝ // ContinuousOn g (Set.Icc 0 1) } → ℝ), True

Example 0.3.12: Functions between spaces of functions include the derivative sending a differentiable real function to another real function, the Laplace transform viewed as a function taking functions to functions, and the definite integral assigning a number to a continuous function on [0,1].

@[reducible, inline]

abbrev directImageElementCollection {α : Type u} {β : Type v} (f : α → β) (C : Set α) : Set β

Definition 0.3.13: For a function f : A → B, the image (direct image) of C ⊆ A is f(C) = { f x ∈ B | x ∈ C }, and the inverse image of D ⊆ B is f ⁻¹(D) = { x ∈ A | f x ∈ D }.

Equations

• directImageElementCollection f C = f '' C

theorem directImageElementCollection_eq {α : Type u} {β : Type v} (f : α → β) (C : Set α) : directImageElementCollection f C = f '' C

The book's image of a subset is mathlib's Set.image.

@[reducible, inline]

abbrev inverseImageElementCollection {α : Type u} {β : Type v} (f : α → β) (D : Set β) : Set α

The inverse image of a subset under f.

Equations

• inverseImageElementCollection f D = f ⁻¹' D

theorem inverseImageElementCollection_eq {α : Type u} {β : Type v} (f : α → β) (D : Set β) : inverseImageElementCollection f D = f ⁻¹' D

The book's inverse image coincides with mathlib's preimage.

noncomputable def sinPiFunction : ℝ → ℝ

Example 0.3.14: For f(x) = sin (π x), one has f([0, 1/2]) = [0, 1] and f ⁻¹({0}) = ℤ, etc.

Equations

• sinPiFunction x = Real.sin (Real.pi * x)

theorem sinPiFunction_image_subset_Icc : sinPiFunction '' Set.Icc 0 (1 / 2) ⊆ Set.Icc 0 1

Helper: values of sin (π x) on [0, 1/2] lie in [0, 1].

theorem sinPiFunction_surj_Icc : Set.Icc 0 1 ⊆ sinPiFunction '' Set.Icc 0 (1 / 2)

Helper: every y ∈ [0,1] is of the form sin (π x) for some x ∈ [0,1/2].

theorem sinPiFunction_image_half_interval : sinPiFunction '' Set.Icc 0 (1 / 2) = Set.Icc 0 1

Example 0.3.14: The image of [0, 1/2] under x ↦ sin (π x) is [0, 1].

theorem sinPiFunction_preimage_zero_iff (x : ℝ) : sinPiFunction x = 0 ↔ ∃ (n : ℤ), ↑n = x

Helper: sin (π x) = 0 iff x is an integer.

theorem sinPiFunction_preimage_zero : sinPiFunction ⁻¹' {0} = Set.range fun (n : ℤ) => ↑n

Example 0.3.14: The preimage of {0} under x ↦ sin (π x) is the set of integers.

theorem preimage_union_inter_compl {α : Type u} {β : Type v} {f : α → β} {C D : Set β} : f ⁻¹' (C ∪ D) = f ⁻¹' C ∪ f ⁻¹' D ∧ f ⁻¹' (C ∩ D) = f ⁻¹' C ∩ f ⁻¹' D ∧ f ⁻¹' Cᶜ = (f ⁻¹' C)ᶜ

Proposition 0.3.15: For a function f : A → B and subsets C, D of B, f ⁻¹'(C ∪ D) = f ⁻¹' C ∪ f ⁻¹' D, f ⁻¹'(C ∩ D) = f ⁻¹' C ∩ f ⁻¹' D, and f ⁻¹'(Cᶜ) = (f ⁻¹' C)ᶜ.

theorem image_union_inter_subset {α : Type u} {β : Type v} {f : α → β} {C D : Set α} : f '' (C ∪ D) = f '' C ∪ f '' D ∧ f '' (C ∩ D) ⊆ f '' C ∩ f '' D

Proposition 0.3.16: For a function f : A → B and subsets C, D of A, f (C ∪ D) = f (C) ∪ f (D) and f (C ∩ D) ⊆ f (C) ∩ f (D).

@[reducible, inline]

abbrev injectiveFunction {α : Type u} {β : Type v} (f : α → β) : Prop

Definition 0.3.17: A function f : A → B is injective (one-to-one) if f x₁ = f x₂ implies x₁ = x₂, equivalently each fiber f ⁻¹' {y} is empty or a singleton; it is surjective (onto) if f(A) = B, i.e., its range equals its codomain; it is bijective if both.

Equations

• injectiveFunction f = Function.Injective f

theorem injectiveFunction_iff {α : Type u} {β : Type v} {f : α → β} : injectiveFunction f ↔ Function.Injective f

The book's injectivity is mathlib's Function.Injective.

@[reducible, inline]

abbrev surjectiveFunction {α : Type u} {β : Type v} (f : α → β) : Prop

The book's notion of surjective function.

Equations

• surjectiveFunction f = Function.Surjective f

theorem surjectiveFunction_iff {α : Type u} {β : Type v} {f : α → β} : surjectiveFunction f ↔ Function.Surjective f

The book's surjectivity coincides with mathlib's Function.Surjective.

@[reducible, inline]

abbrev bijectiveFunction {α : Type u} {β : Type v} (f : α → β) : Prop

The book's bijection is a function that is both injective and surjective.

Equations

• bijectiveFunction f = Function.Bijective f

theorem bijectiveFunction_iff {α : Type u} {β : Type v} {f : α → β} : bijectiveFunction f ↔ Function.Bijective f

The book's bijectivity is mathlib's Function.Bijective.

@[reducible, inline]

abbrev functionComposition {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) : α → γ

Definition 0.3.18: For functions f : A → B and g : B → C, the composition g ∘ f : A → C is given by (g ∘ f) x = g (f x).

Equations

• functionComposition g f = g ∘ f

theorem functionComposition_eq {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) : functionComposition g f = g ∘ f

The book's composition of functions is mathlib's function composition.

theorem functionComposition_apply {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (x : α) : functionComposition g f x = g (f x)