r
/
bookshelf
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Normalize header sizes.

finite-set-exercises
Joshua Potter 2023-06-29 17:02:20 -06:00
parent e869d6f2d3
commit 63667c22e4
2 changed files with 43 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
Bookshelf/Enderton/Set/Chapter_2.lean
View File

@ -10,7 +10,7 @@ Axioms and Operations
namespace Enderton.Set.Chapter_2 namespace Enderton.Set.Chapter_2
/-- ### Exercise 2.1 /-- #### Exercise 2.1
Assume that `A` is the set of integers divisible by `4`. Similarly assume that Assume that `A` is the set of integers divisible by `4`. Similarly assume that
`B` and `C` are the sets of integers divisible by `9` and `10`, respectively. `B` and `C` are the sets of integers divisible by `9` and `10`, respectively.
@ -32,7 +32,7 @@ theorem exercise_2_1 {A B C : Set ℤ}
· rw [hC] at hc · rw [hC] at hc
exact Set.mem_setOf.mp hc exact Set.mem_setOf.mp hc
/-- ### Exercise 2.2 /-- #### Exercise 2.2
Give an example of sets `A` and `B` for which `⋃ A = ⋃ B` but `A ≠ B`. Give an example of sets `A` and `B` for which `⋃ A = ⋃ B` but `A ≠ B`.
-/ -/
@ -71,7 +71,7 @@ theorem exercise_2_2 {A B : Set (Set ℕ)}
have h₂ := h₁ 2 have h₂ := h₁ 2
simp at h₂ simp at h₂
/-- ### Exercise 2.3 /-- #### Exercise 2.3
Show that every member of a set `A` is a subset of `U A`. (This was stated as an Show that every member of a set `A` is a subset of `U A`. (This was stated as an
example in this section.) example in this section.)
@ -84,7 +84,7 @@ theorem exercise_2_3 {A : Set (Set α)}
rw [Set.mem_setOf_eq] rw [Set.mem_setOf_eq]
exact ⟨x, ⟨hx, hy⟩⟩ exact ⟨x, ⟨hx, hy⟩⟩
/-- ### Exercise 2.4 /-- #### Exercise 2.4
Show that if `A ⊆ B`, then `⋃ A ⊆ ⋃ B`. Show that if `A ⊆ B`, then `⋃ A ⊆ ⋃ B`.
-/ -/
@ -96,7 +96,7 @@ theorem exercise_2_4 {A B : Set (Set α)} (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B
rw [Set.mem_setOf_eq] rw [Set.mem_setOf_eq]
exact ⟨t, ⟨h ht, hxt⟩⟩ exact ⟨t, ⟨h ht, hxt⟩⟩
/-- ### Exercise 2.5 /-- #### Exercise 2.5
Assume that every member of `𝓐` is a subset of `B`. Show that `⋃ 𝓐 ⊆ B`. Assume that every member of `𝓐` is a subset of `B`. Show that `⋃ 𝓐 ⊆ B`.
-/ -/
@ -108,7 +108,7 @@ theorem exercise_2_5 {𝓐 : Set (Set α)} (h : ∀ x ∈ 𝓐, x ⊆ B)
have ⟨t, ⟨ht𝓐, hyt⟩⟩ := hy have ⟨t, ⟨ht𝓐, hyt⟩⟩ := hy
exact (h t ht𝓐) hyt exact (h t ht𝓐) hyt
/-- ### Exercise 2.6a /-- #### Exercise 2.6a
Show that for any set `A`, `⋃ 𝓟 A = A`. Show that for any set `A`, `⋃ 𝓟 A = A`.
-/ -/
@ -125,7 +125,7 @@ theorem exercise_2_6a : ⋃₀ (𝒫 A) = A := by
rw [Set.mem_setOf_eq] rw [Set.mem_setOf_eq]
exact ⟨A, ⟨by rw [Set.mem_setOf_eq], hx⟩⟩ exact ⟨A, ⟨by rw [Set.mem_setOf_eq], hx⟩⟩
/-- ### Exercise 2.6b /-- #### Exercise 2.6b
Show that `A ⊆ 𝓟 ⋃ A`. Under what conditions does equality hold? Show that `A ⊆ 𝓟 ⋃ A`. Under what conditions does equality hold?
-/ -/
@ -144,7 +144,7 @@ theorem exercise_2_6b
conv => rhs; rw [hB, exercise_2_6a] conv => rhs; rw [hB, exercise_2_6a]
exact hB exact hB
/-- ### Exercise 2.7a /-- #### Exercise 2.7a
Show that for any sets `A` and `B`, `𝓟 A ∩ 𝓟 B = 𝓟 (A ∩ B)`. Show that for any sets `A` and `B`, `𝓟 A ∩ 𝓟 B = 𝓟 (A ∩ B)`.
-/ -/
@ -162,9 +162,7 @@ theorem exercise_2_7A
intro x hA _ intro x hA _
exact hA exact hA
-- theorem false_of_false_iff_true : (false ↔ true) → false := by simp /-- #### Exercise 2.7b (i)
/-- ### Exercise 2.7b (i)
Show that `𝓟 A ∪ 𝓟 B ⊆ 𝓟 (A ∪ B)`. Show that `𝓟 A ∪ 𝓟 B ⊆ 𝓟 (A ∪ B)`.
-/ -/
@ -181,7 +179,7 @@ theorem exercise_2_7b_i
rw [Set.mem_setOf_eq] rw [Set.mem_setOf_eq]
exact Set.subset_union_of_subset_right hB A exact Set.subset_union_of_subset_right hB A
/-- ### Exercise 2.7b (ii) /-- #### Exercise 2.7b (ii)
Under what conditions does `𝓟 A ∪ 𝓟 B = 𝓟 (A ∪ B)`.? Under what conditions does `𝓟 A ∪ 𝓟 B = 𝓟 (A ∪ B)`.?
-/ -/
@ -233,7 +231,7 @@ theorem exercise_2_7b_ii
refine Or.inl (Set.Subset.trans hx ?_) refine Or.inl (Set.Subset.trans hx ?_)
exact subset_of_eq (Set.right_subset_union_eq_self hB) exact subset_of_eq (Set.right_subset_union_eq_self hB)
/-- ### Exercise 2.9 /-- #### Exercise 2.9
Give an example of sets `a` and `B` for which `a ∈ B` but `𝓟 a ∉ 𝓟 B`. Give an example of sets `a` and `B` for which `a ∈ B` but `𝓟 a ∉ 𝓟 B`.
-/ -/
@ -261,7 +259,7 @@ theorem exercise_2_9 (ha : a = {1}) (hB : B = {{1}})
have := h 1 have := h 1
simp at this simp at this
/-- ### Exercise 2.10 /-- #### Exercise 2.10
Show that if `a ∈ B`, then `𝓟 a ∈ 𝓟 𝓟 ⋃ B`. Show that if `a ∈ B`, then `𝓟 a ∈ 𝓟 𝓟 ⋃ B`.
-/ -/
@ -274,7 +272,7 @@ theorem exercise_2_10 {B : Set (Set α)} (ha : a ∈ B)
rw [← hb, Set.mem_setOf_eq] rw [← hb, Set.mem_setOf_eq]
exact h₂ exact h₂
/-- ### Exercise 2.11 (i) /-- #### Exercise 2.11 (i)
Show that for any sets `A` and `B`, `A = (A ∩ B) ∪ (A - B)`. Show that for any sets `A` and `B`, `A = (A ∩ B) ∪ (A - B)`.
-/ -/
@ -291,7 +289,7 @@ theorem exercise_2_11_i {A B : Set α}
· intro hx · intro hx
exact ⟨hx, em (B x)⟩ exact ⟨hx, em (B x)⟩
/-- ### Exercise 2.11 (ii) /-- #### Exercise 2.11 (ii)
Show that for any sets `A` and `B`, `A ∪ (B - A) = A ∪ B`. Show that for any sets `A` and `B`, `A ∪ (B - A) = A ∪ B`.
-/ -/
@ -385,7 +383,7 @@ lemma left_diff_eq_singleton_one : (A \ B) \ C = {1} := by
| inl y => rw [hx] at y; simp at y | inl y => rw [hx] at y; simp at y
| inr y => rw [hx] at y; simp at y | inr y => rw [hx] at y; simp at y
/-- ### Exercise 2.14 /-- #### Exercise 2.14
Show by example that for some sets `A`, `B`, and `C`, the set `A - (B - C)` is Show by example that for some sets `A`, `B`, and `C`, the set `A - (B - C)` is
different from `(A - B) - C`. different from `(A - B) - C`.
@ -402,7 +400,7 @@ theorem exercise_2_14 : A \ (B \ C) ≠ (A \ B) \ C := by
end end
/-- ### Exercise 2.16 /-- #### Exercise 2.16
Simplify: Simplify:
`[(A ∪ B ∪ C) ∩ (A ∪ B)] - [(A ∪ (B - C)) ∩ A]` `[(A ∪ B ∪ C) ∩ (A ∪ B)] - [(A ∪ (B - C)) ∩ A]`
@ -414,7 +412,7 @@ theorem exercise_2_16 {A B C : Set α}
_ = (A ∪ B) \ A := by rw [Set.union_inter_cancel_left] _ = (A ∪ B) \ A := by rw [Set.union_inter_cancel_left]
_ = B \ A := by rw [Set.union_diff_left] _ = B \ A := by rw [Set.union_diff_left]
/-! ### Exercise 2.17 /-! #### Exercise 2.17
Show that the following four conditions are equivalent. Show that the following four conditions are equivalent.
@ -450,7 +448,7 @@ theorem exercise_2_17_iii {A B : Set α} (h : A ∪ B = B)
theorem exercise_2_17_iv {A B : Set α} (h : A ∩ B = A) theorem exercise_2_17_iv {A B : Set α} (h : A ∩ B = A)
: A ⊆ B := Set.inter_eq_left_iff_subset.mp h : A ⊆ B := Set.inter_eq_left_iff_subset.mp h
/-- ### Exercise 2.19 /-- #### Exercise 2.19
Is `𝒫 (A - B)` always equal to `𝒫 A - 𝒫 B`? Is it ever equal to `𝒫 A - 𝒫 B`? Is `𝒫 (A - B)` always equal to `𝒫 A - 𝒫 B`? Is it ever equal to `𝒫 A - 𝒫 B`?
-/ -/
@ -463,7 +461,7 @@ theorem exercise_2_19 {A B : Set α}
have := h ∅ have := h ∅
exact absurd (this.mp he) ne exact absurd (this.mp he) ne
/-- ### Exercise 2.20 /-- #### Exercise 2.20
Let `A`, `B`, and `C` be sets such that `A ∪ B = A ∪ C` and `A ∩ B = A ∩ C`. Let `A`, `B`, and `C` be sets such that `A ∪ B = A ∪ C` and `A ∩ B = A ∩ C`.
Show that `B = C`. Show that `B = C`.
@ -489,7 +487,7 @@ theorem exercise_2_20 {A B C : Set α}
rw [← hu] at this rw [← hu] at this
exact Or.elim this (absurd · hA) (by simp) exact Or.elim this (absurd · hA) (by simp)
/-- ### Exercise 2.21 /-- #### Exercise 2.21
Show that `⋃ (A ∪ B) = (⋃ A) ∪ (⋃ B)`. Show that `⋃ (A ∪ B) = (⋃ A) ∪ (⋃ B)`.
-/ -/
@ -513,7 +511,7 @@ theorem exercise_2_21 {A B : Set (Set α)}
have ⟨t, ht⟩ : ∃ t, t ∈ B ∧ x ∈ t := hB have ⟨t, ht⟩ : ∃ t, t ∈ B ∧ x ∈ t := hB
exact ⟨t, ⟨Set.mem_union_right A ht.left, ht.right⟩⟩ exact ⟨t, ⟨Set.mem_union_right A ht.left, ht.right⟩⟩
/-- ### Exercise 2.22 /-- #### Exercise 2.22
Show that if `A` and `B` are nonempty sets, then `⋂ (A ∪ B) = ⋂ A ∩ ⋂ B`. Show that if `A` and `B` are nonempty sets, then `⋂ (A ∪ B) = ⋂ A ∩ ⋂ B`.
-/ -/
@ -542,7 +540,7 @@ theorem exercise_2_22 {A B : Set (Set α)}
· intro hB · intro hB
exact (this t).right hB exact (this t).right hB
/-- ### Exercise 2.24a /-- #### Exercise 2.24a
Show that is `𝓐` is nonempty, then `𝒫 (⋂ 𝓐) = ⋂ { 𝒫 X | X ∈ 𝓐 }`. Show that is `𝓐` is nonempty, then `𝒫 (⋂ 𝓐) = ⋂ { 𝒫 X | X ∈ 𝓐 }`.
-/ -/
@ -561,7 +559,7 @@ theorem exercise_2_24a {𝓐 : Set (Set α)}
_ = { x | ∀ t ∈ { 𝒫 X | X ∈ 𝓐 }, x ∈ t} := by simp _ = { x | ∀ t ∈ { 𝒫 X | X ∈ 𝓐 }, x ∈ t} := by simp
_ = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := rfl _ = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := rfl
/-- ### Exercise 2.24b /-- #### Exercise 2.24b
Show that Show that
``` ```
@ -603,7 +601,7 @@ theorem exercise_2_24b {𝓐 : Set (Set α)}
simp only [Set.mem_setOf_eq, exists_exists_and_eq_and, Set.mem_powerset_iff] simp only [Set.mem_setOf_eq, exists_exists_and_eq_and, Set.mem_powerset_iff]
exact ⟨⋃₀ 𝓐, ⟨hA, hx⟩⟩ exact ⟨⋃₀ 𝓐, ⟨hA, hx⟩⟩
/-- ### Exercise 2.25 /-- #### Exercise 2.25
Is `A ∪ (⋃ 𝓑)` always the same as `⋃ { A ∪ X | X ∈ 𝓑 }`? If not, then under Is `A ∪ (⋃ 𝓑)` always the same as `⋃ { A ∪ X | X ∈ 𝓑 }`? If not, then under
what conditions does equality hold? what conditions does equality hold?

38
Bookshelf/Enderton/Set/Chapter_3.lean
View File

@ -9,7 +9,7 @@ Relations and Functions
namespace Enderton.Set.Chapter_3 namespace Enderton.Set.Chapter_3
/-- ### Theorem 3B /-- #### Theorem 3B
If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`. If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`.
-/ -/
@ -19,7 +19,7 @@ theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
exact Set.mem_mem_imp_pair_subset hxs hxys exact Set.mem_mem_imp_pair_subset hxs hxys
/-- ### Exercise 3.1 /-- #### Exercise 3.1
Suppose that we attempted to generalize the Kuratowski definitions of ordered Suppose that we attempted to generalize the Kuratowski definitions of ordered
pairs to ordered triples by defining pairs to ordered triples by defining
@ -42,7 +42,7 @@ theorem exercise_3_1 {x y z u v w : ℕ}
· rw [hy, hv] · rw [hy, hv]
simp only simp only
/-- ### Exercise 3.2a /-- #### Exercise 3.2a
Show that `A × (B ∪ C) = (A × B) ∪ (A × C)`. Show that `A × (B ∪ C) = (A × B) ∪ (A × C)`.
-/ -/
@ -58,7 +58,7 @@ theorem exercise_3_2a {A : Set α} {B C : Set β}
_ = { p | p ∈ Set.prod A B ∨ (p ∈ Set.prod A C) } := rfl _ = { p | p ∈ Set.prod A B ∨ (p ∈ Set.prod A C) } := rfl
_ = (Set.prod A B) ∪ (Set.prod A C) := rfl _ = (Set.prod A B) ∪ (Set.prod A C) := rfl
/-- ### Exercise 3.2b /-- #### Exercise 3.2b
Show that if `A × B = A × C` and `A ≠ ∅`, then `B = C`. Show that if `A × B = A × C` and `A ≠ ∅`, then `B = C`.
-/ -/
@ -87,7 +87,7 @@ theorem exercise_3_2b {A : Set α} {B C : Set β}
have ⟨c, hc⟩ := Set.nonempty_iff_ne_empty.mpr (Ne.symm nC) have ⟨c, hc⟩ := Set.nonempty_iff_ne_empty.mpr (Ne.symm nC)
exact (h (a, c)).mpr ⟨ha, hc⟩ exact (h (a, c)).mpr ⟨ha, hc⟩
/-- ### Exercise 3.3 /-- #### Exercise 3.3
Show that `A × ⋃ 𝓑 = ⋃ {A × X | X ∈ 𝓑}`. Show that `A × ⋃ 𝓑 = ⋃ {A × X | X ∈ 𝓑}`.
-/ -/
@ -115,7 +115,7 @@ theorem exercise_3_3 {A : Set (Set α)} {𝓑 : Set (Set β)}
· intro ⟨b, h₁, h₂, h₃⟩ · intro ⟨b, h₁, h₂, h₃⟩
exact ⟨b, h₁, h₂, h₃⟩ exact ⟨b, h₁, h₂, h₃⟩
/-- ### Exercise 3.5a /-- #### Exercise 3.5a
Assume that `A` and `B` are given sets, and show that there exists a set `C` Assume that `A` and `B` are given sets, and show that there exists a set `C`
such that for any `y`, such that for any `y`,
@ -183,7 +183,7 @@ theorem exercise_3_5a {A : Set α} {B : Set β}
rw [hab.right] rw [hab.right]
exact ⟨hab.left, hb⟩ exact ⟨hab.left, hb⟩
/-- ### Exercise 3.5b /-- #### Exercise 3.5b
With `A`, `B`, and `C` as above, show that `A × B = ∪ C`. With `A`, `B`, and `C` as above, show that `A × B = ∪ C`.
-/ -/
@ -216,7 +216,7 @@ theorem exercise_3_5b {A : Set α} (B : Set β)
rw [← ha] at h rw [← ha] at h
exact ⟨h, hb⟩ exact ⟨h, hb⟩
/-- ### Theorem 3D /-- #### Theorem 3D
If `⟨x, y⟩ ∈ A`, then `x` and `y` belong to `⋃ ⋃ A`. If `⟨x, y⟩ ∈ A`, then `x` and `y` belong to `⋃ ⋃ A`.
-/ -/
@ -228,7 +228,7 @@ theorem theorem_3d {A : Set (Set (Set α))} (h : OrderedPair x y ∈ A)
have : {x, y} ⊆ ⋃₀ ⋃₀ A := Chapter_2.exercise_2_3 {x, y} hq have : {x, y} ⊆ ⋃₀ ⋃₀ A := Chapter_2.exercise_2_3 {x, y} hq
exact ⟨this (by simp), this (by simp)⟩ exact ⟨this (by simp), this (by simp)⟩
/-- ### Exercise 3.6 /-- #### Exercise 3.6
Show that a set `A` is a relation **iff** `A ⊆ dom A × ran A`. Show that a set `A` is a relation **iff** `A ⊆ dom A × ran A`.
-/ -/
@ -246,7 +246,7 @@ theorem exercise_3_6 {A : Set.Relation α}
] ]
exact ⟨⟨b, ht⟩, ⟨a, ht⟩⟩ exact ⟨⟨b, ht⟩, ⟨a, ht⟩⟩
/-- ### Exercise 3.7 /-- #### Exercise 3.7
Show that if `R` is a relation, then `fld R = ⋃ ⋃ R`. Show that if `R` is a relation, then `fld R = ⋃ ⋃ R`.
-/ -/
@ -329,7 +329,7 @@ section
open Set.Relation open Set.Relation
/-- ### Exercise 3.8 (i) /-- #### Exercise 3.8 (i)
Show that for any set `𝓐`: Show that for any set `𝓐`:
``` ```
@ -355,7 +355,7 @@ theorem exercise_3_8_i {A : Set (Set.Relation α)}
· intro ⟨t, ht, y, hx⟩ · intro ⟨t, ht, y, hx⟩
exact ⟨y, t, ht, hx⟩ exact ⟨y, t, ht, hx⟩
/-- ### Exercise 3.8 (ii) /-- #### Exercise 3.8 (ii)
Show that for any set `𝓐`: Show that for any set `𝓐`:
``` ```
@ -380,7 +380,7 @@ theorem exercise_3_8_ii {A : Set (Set.Relation α)}
· intro ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩ · intro ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩
exact ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩ exact ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩
/-- ### Exercise 3.9 (i) /-- #### Exercise 3.9 (i)
Discuss the result of replacing the union operation by the intersection Discuss the result of replacing the union operation by the intersection
operation in the preceding problem. operation in the preceding problem.
@ -406,7 +406,7 @@ theorem exercise_3_9_i {A : Set (Set.Relation α)}
intro _ y hy R hR intro _ y hy R hR
exact ⟨y, hy R hR⟩ exact ⟨y, hy R hR⟩
/-- ### Exercise 3.9 (ii) /-- #### Exercise 3.9 (ii)
Discuss the result of replacing the union operation by the intersection Discuss the result of replacing the union operation by the intersection
operation in the preceding problem. operation in the preceding problem.
@ -432,7 +432,7 @@ theorem exercise_3_9_ii {A : Set (Set.Relation α)}
intro _ y hy R hR intro _ y hy R hR
exact ⟨y, hy R hR⟩ exact ⟨y, hy R hR⟩
/-- ### Theorem 3G (i) /-- #### Theorem 3G (i)
Assume that `F` is a one-to-one function. If `x ∈ dom F`, then `F⁻¹(F(x)) = x`. Assume that `F` is a one-to-one function. If `x ∈ dom F`, then `F⁻¹(F(x)) = x`.
-/ -/
@ -446,7 +446,7 @@ theorem theorem_3g_i {F : Set.Relation α}
unfold isOneToOne at hF unfold isOneToOne at hF
exact (single_valued_eq_unique hF.left hy hy₁).symm exact (single_valued_eq_unique hF.left hy hy₁).symm
/-- ### Theorem 3G (ii) /-- #### Theorem 3G (ii)
Assume that `F` is a one-to-one function. If `y ∈ ran F`, then `F(F⁻¹(y)) = y`. Assume that `F` is a one-to-one function. If `y ∈ ran F`, then `F(F⁻¹(y)) = y`.
-/ -/
@ -460,7 +460,7 @@ theorem theorem_3g_ii {F : Set.Relation α}
unfold isOneToOne at hF unfold isOneToOne at hF
exact (single_rooted_eq_unique hF.right hx hx₁).symm exact (single_rooted_eq_unique hF.right hx hx₁).symm
/-- ### Theorem 3H /-- #### Theorem 3H
Assume that `F` and `G` are functions. Then Assume that `F` and `G` are functions. Then
``` ```
@ -500,7 +500,7 @@ theorem theorem_3h_dom {F G : Set.Relation α}
simp only [Set.mem_setOf_eq] simp only [Set.mem_setOf_eq]
exact ⟨a, ha.left.left, hb⟩ exact ⟨a, ha.left.left, hb⟩
/-- ### Theorem 3J (a) /-- #### Theorem 3J (a)
Assume that `F : A → B`, and that `A` is nonempty. There exists a function Assume that `F : A → B`, and that `A` is nonempty. There exists a function
`G : B → A` (a "left inverse") such that `G ∘ F` is the identity function on `A` `G : B → A` (a "left inverse") such that `G ∘ F` is the identity function on `A`
@ -512,7 +512,7 @@ theorem theorem_3j_a {F : Set.Relation α} {A B : Set α}
G.mapsInto B A ∧ (∀ p ∈ G.comp F, p.1 = p.2)) ↔ F.isOneToOne := by G.mapsInto B A ∧ (∀ p ∈ G.comp F, p.1 = p.2)) ↔ F.isOneToOne := by
sorry sorry
/-- ### Theorem 3J (b) /-- #### Theorem 3J (b)
Assume that `F : A → B`, and that `A` is nonempty. There exists a function Assume that `F : A → B`, and that `A` is nonempty. There exists a function
`H : B → A` (a "right inverse") such that `F ∘ H` is the identity function on `H : B → A` (a "right inverse") such that `F ∘ H` is the identity function on