fix: correct false continuity example and disambiguate exercise labels

[Chessing234]

Summary

• Fix Exercise 11.5.1: 1/x is not continuous on [0,1] — state ¬ ContinuousOn and label both parts.
• Label both Exercise 11.6.4 integral-test counterexamples as parts (a) and (b).
• Disambiguate duplicate Verso labels in Exercises 11.3.1 and 3.1.7–3.1.9.

Test plan

• lake build Analysis succeeds
• Spot-check Verso anchors for Ex. 11.3.1, 11.5.1, 11.6.4, and 3.1.7–3.1.9

Made with Cursor

[teorth]

Thanks — the Exercise 11.5.1 catch here was a real one, and I've landed it separately in #620 with credit to you. ContinuousOn (fun x ↦ 1/x) (Icc 0 1) was genuinely false, so that sorry was unprovable.

I'm closing this PR rather than merging it, because the rest of the changes are docstring disambiguation, and that premise doesn't hold for this repo. Repeated identical exercise docstrings are intentional house style — 12x /-- Exercise 5.4.9 -/, 6x /-- Exercise 3.5.4 -/, and so on — and there's no label or anchor machinery keyed on docstring text (literate.toml sets docstrings_as_text = true, so anchors come from declaration names). That's also why CI was green: there was nothing being fixed. This PR had also gone out of date, with conflicts in Sections 11.3 and 11.5.

If you'd like to propose changing the convention, please open an issue so it can be settled repo-wide.

Statement corrections like the 11.5.1 one — false or mis-hypothesized sorryd goals, in the spirit of #517 — remain very welcome, and are best sent on their own rather than bundled with cosmetic edits.

[teorth]

Reopening — please disregard my previous comment, which was wrong.

I assessed this against a stale checkout of main that was roughly 200 commits behind origin/main. The duplicate-docstring counts I cited (12x /-- Exercise 5.4.9 -/ and so on) were from that stale tree; those had already been fixed on main by #616 and the other label PRs. The label-disambiguation work is an active and accepted cleanup here, not a departure from house style, and this PR is a legitimate continuation of it.

Apologies for the noise.