Explanation about Inverse function in Chapter 4

[yannickseurin]

Chapter 4 presents the definition of the inverse of a function in Section 4.2:

With these in hand, we can define the inverse function as follows:

noncomputable section

open Classical

def inverse (f : α → β) : β → α := fun y : β ↦
  if h : ∃ x, f x = y then Classical.choose h else default

theorem inverse_spec {f : α → β} (y : β) (h : ∃ x, f x = y) : f (inverse f y) = y := by
 rw [inverse, dif_pos h]
 exact Classical.choose_spec h

Later in Section 4.3, the inverse function is presented once again without reference to the previous section (e.g. without relating inverse in Section 4.2 and invFun in Section 4.3, or inverse_spec and invFun_eq in Section 4.3), which sounds odd:

Specifically, we need the hypothesis [Nonempty β] for the operation invFun that is defined in Mathlib. Given x : α, invFun g x chooses a preimage of x in β if there is one, and returns an arbitrary element of β otherwise. The function invFun g is always a left inverse if g is injective and a right inverse if g is surjective.

#check (invFun g : α → β)
#check (leftInverse_invFun : Injective g → LeftInverse (invFun g) g)
#check (leftInverse_invFun : Injective g → ∀ y, invFun g (g y) = y)
#check (invFun_eq : (∃ y, g y = x) → g (invFun g x) = x)

It sounds as if the end of Section 4.2 has been added after Section 4.3.