fix: continuous const/id examples; 1/x not continuous on [0,1]

[Chessing234]

Summary

• Prove Convergesto.const / Convergesto.id and fill Examples 9.4.2–9.4.3 (constant and identity continuity).
• Prove ¬ ContinuousOn (fun x ↦ 1/x) (Icc 0 1), closing the sorry left after fix: ContinuousOn 1/x on [0,1] is false; split Ex. 11.3.1 labels #613 corrected the false positive claim.

Test plan

• CI build

[teorth]

Thanks for the careful work here — but I am going to decline this one on policy grounds rather than on its merits.

This PR discharges eight sorrys in Analysis/Section_11_5.lean, Analysis/Section_9_3.lean and Analysis/Section_9_4.lean with full proofs. Those sorrys are the exercises left to the reader, and the repository deliberately does not carry their solutions:

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

CONTRIBUTING.md — "However, I do not intend to place solutions in this repository directly."

The intended home for this kind of work is a downstream fork — and per CONTRIBUTING.md that "playtesting" is genuinely wanted, including feedback on whether the helper lemmas and API provided here are enough to fill the sorries in a conceptually straightforward way. Reports of places where they are not would be very welcome as issues.

Note that Analysis/MeasureTheory/ is different: its README says "Readers who are not in my classes are also welcome to submit such proofs." So proofs are accepted there, just not in the Analysis I sections.

Two notes in case they are useful for your fork:

• CI was failing on a genuine error, not infrastructure. At Section_11_5.lean:107 the term (one_div_le_one_div _ hxpos).mp hx_le_half runs that iff the wrong way — hx_le_half : x ≤ 1/2 is being supplied where 1/(1/2) ≤ 1/x is expected. one_div_le_one_div_of_le hxpos hx_le_half gives the inequality directly.
• The ¬ ContinuousOn (fun x ↦ 1/x) (Icc 0 1) statement you were proving is the one you correctly flagged and fix: ContinuousOn 1/x on [0,1] is false; split Ex. 11.3.1 labels #613 fixed — thank you for that; the statement correction was exactly the kind of contribution that is wanted here.

Your statement-correction PRs remain very welcome, and several are queued and being reviewed.

[Chessing234]

understood — won't push Analysis/ exercise solutions upstream. kept the one_div_le_one_div_of_le fix on the fork tip only.