Section 9.8: fix undecidable Exercise 9.8.4 statements from issue #517

[Chessing234]

Summary

Fixes the two Exercise 9.8.4 Decidable exercises flagged in #517.

Previously the parameters (a, b, f, and the continuity/monotonicity hypotheses) were bound outside the Decidable, so the decided proposition depended on the specific function — making it true for some admissible inputs and false for others, i.e. not uniformly decidable.

Per @teorth's suggestion, the quantification is now moved inside the Decidable, so each exercise decides a single closed universal statement (in the spirit of the textbook's "is this true or false?" exercise):

• exist_inverse_without_continuity: decide whether strict monotonicity alone yields a (continuous, strict-mono) inverse.
• exist_inverse_without_strictmono: decide whether continuity + monotonicity (without strictness) yields such an inverse.

Test plan

• lake build (signature-only change)

[teorth]

To be closer to the spirit of the exercise, one can move the quantification over the parameters a, b, f, hcont, hmono inside the Decidable statement instead.

[Chessing234]

Good call — pushed an update that keeps the Decidable form but quantifies a, b, f (and the mono/continuity hypotheses) inside the proposition. The student step is then uniformly isFalse for both variants.

[Chessing234]

Thanks — done. Both exercises now keep the Decidable formulation with the quantification over a, b, f (and the continuity / monotonicity hypotheses) moved inside the decided proposition, so each statement is a self-contained "decide whether this universal claim holds" as intended.

[daikonradish]

hi @Chessing234, i started work on this section also and came to flag this problem, as i was stuck unable to prove. is there a way that you could fix the build failure so i can pull the code? in particular i think your code is not compiling because it's Set.Icc or .Icc, but you've used Icc.,

[Chessing234]

Rebased onto current main.

[Chessing234]

Fixed CI: bare Icc → .Icc in universal Ex. 9.8.4 Decidable statements.