Exercise 3.5.12 question

Stream: Analysis I

[Brandon]

Disclaimer: I am a beginner when it comes to both math and Lean.

I am quite perplexed by exercise 3.5.12:
image.png

After proving via induction that for any N, there exists a function with a bounded domain up to N that fulfills the desired properties, we still need to show there exists a function that works for the unbounded domain of naturals.

My assumption is that the intended solution is to then define such a function as a(n) = a'n(n) where a' are the bounded functions defined inductively above. In Lean, this might look something like:

have h_bounded : ∀ n': ℕ, ∃ a: Fin (n'+1) → X, ...
use fun n:nat ↦ (h_bounded n).choose ⟨ n, by ... ⟩

While Lean accepts this, I believe this approach is incorrect as it involves the axiom of choice? My only knowledge of what the axiom is comes from the same chapter:
image.png

It sounds like we're making an infinite number of choices and using this same technique, I can prove the unbounded version of the lemma that the remark is saying cannot be proven yet.

Therefore, I'm guessing this is not the intended solution. But I also cannot for the life of me figure out what is. Any gentle nudge towards the right direction would be greatly appreciated :D

[Brandon]

Or actually, if you define h_bounded as exists unique, does this suddenly become an operation that doesn't involve axiom of choice?

[Aaron Liu]

The reason that in the set theory, this does not need choice, is that all the existence is unique. So you are not "really" making any choices, since there is only one thing to choose each time. Functions are implemented as a special type of relation, and unique choice is an easy lemma. However the way Lean's type theory works is somewhat different. A function according to Lean is a something that takes inputs of the correct type and constructs an output of the correct type. Since we actually need to construct the value, proving existence (even unique existence) is not enough on its own, you also need the axiom of choice to "construct" the output given a proof of existence.

[Terence Tao]

Some related discussion: #Analysis I > Using axiom of choice in chapters 2 and 3 and .choose