fix: refute Ex. 9.8.4 without StrictMono; label §6.3 examples

[Chessing234]

Summary

• Prove Exercise 9.8.4 without strict monotonicity is false (apply isFalse): constant f ≡ 0 on [0,1] is continuous and monotone but admits no left inverse
• Disambiguate duplicate Verso labels for Examples 6.3.3–6.3.5 and Remark 6.3.7

Test plan

• lake build Analysis.Section_9_8
• lake build Analysis.Section_6_3

[Chessing234]

ex 9.8.4 false-sorry + §6.3 labels are on tip; happy to split if you'd rather land labels separately.

[teorth]

The Section 6.3 half of this is good and I would happily take it — but the Analysis/Section_9_8.lean hunk discharges the sorry in MonotoneOn.exist_inverse_without_strictmono with a full apply isFalse; … proof, and the repository deliberately does not carry solutions to the Analysis I exercises:

README.md — "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."

Note that the line you replaced was the hint left for the reader (-- apply isFalse: e.g. a constant monotone f on [a,b] has no strict inverse), which is exactly the part the exercise is asking them to supply.

Please do resubmit the Section 6.3 labels on their own — Example 6.3.3/6.3.4/6.3.5 (a)/(b) and Remark 6.3.7 (a)/(b)/(c). I checked those against the text: Examples 6.3.3–6.3.5 are each a single prose example asserting a sup and an inf, and Remark 6.3.7 is the dual of the three claims of Proposition 6.3.6, so the counts line up and lettered parts match the convention the book uses predominantly. That half would merge as-is. (#627, which labels Propositions 6.3.6/6.3.8 and Example 6.3.9 in the same file, has just been merged, so it will need a rebase.)

Analysis/MeasureTheory/ is the exception to the solutions policy — its README says "Readers who are not in my classes are also welcome to submit such proofs." The restriction is only on the Analysis I sections.

[Chessing234]

resubmitted the §6.3 labels alone as #633 (no 9.8.4 solution).