Disprove Exercise 9.8.4 variants that drop continuity or strict mono

[Chessing234]

Summary

• Prove MonotoneOn.exist_inverse_without_continuity and exist_inverse_without_strictmono are false statements via isFalse.
• Jump discontinuity on [0,2] is strictly mono but does not fill [f 0, f 2].
• Constant map is continuous and monotone but has no left inverse.

Test plan

• CI / lake build for Analysis/Section_9_8.lean

[teorth]

Thank you for this batch, and please read this as redirection rather than rejection — your work on this repository has been genuinely valuable and I'd like it to keep coming.

I'm closing this PR and fourteen siblings (#668–#673, #675–#677, #680–#684) under the repository's solutions policy. From the README:

Portions of the text that were left as exercises to the reader are rendered in this translation as sorrys. Readers are welcome to fork the repository here to try their hand at these exercises, but I do not intend to place solutions in this repository directly.

and CONTRIBUTING:

I would be interested in having volunteers "playtest" the companion (using downstream forks of the repository) ... However, I do not intend to place solutions in this repository directly.

Each of these fifteen PRs discharges one or more Analysis I reader exercises and deletes the hint comment that goes with it — "the first line of this construction should be either apply isTrue or apply isFalse, depending on whether you believe the given statement to be true or false." That comment is the exercise: deciding which way it goes is the work being asked of the reader. I checked all fifteen and none of them changes a statement, so they are solutions rather than corrections.

I want to be clear about what the policy is not saying, because the distinction matters and you have been on the right side of it repeatedly:

• Statement corrections are very welcome, including in Analysis I. When a Lean statement is false, or drifts from the text, fixing the statement and leaving the sorry in place is exactly right. fix: Exercise 10.2.6 should bound |f x - f y| on the closed interval #674 in this same batch is a good example — Exercise 10.2.6 quantified over Set.Ioo a b where ch10 says "for any $x, y \in [a,b]$" — and it's merged.
• Proofs in Analysis/MeasureTheory/ are welcome, and its README says so explicitly: "Readers who are not in my classes are also welcome to submit such proofs." feat(MeasureTheory): prove elementary and Jordan product measures #665 and feat(MeasureTheory): prove the TFAE characterizations of Jordan measurability #666 from this batch are merged.
• Bug reports about false statements are welcome even when the fix is unclear. fix: require boundedness for Lebesgue=Jordan-inner equalities #679 is a good instance and I've left it open with a comment.

So the boundary is Analysis I sorrys specifically. If, while solving one of these in your fork, you find that the Lean statement is wrong — which is how several of your best PRs started — a PR that fixes the statement and keeps the sorry is the ideal contribution.

Two other things still open on your side, both small: #652, #654 and #658 need the invented (a)/(b) part labels on prose example blocks swapped for descriptive parentheticals (details on each PR), and #640 is still labelling Proposition 5.4.4's seven declarations (a)–(g) where the book's (a),(b),(c) are the three trichotomy alternatives.

Thanks again — the statement-correction and measure-theory work has been a real contribution.