fix: label Ex. 11.5.1/Example 11.5.5; tidy Lusin docstring

[Chessing234]

Summary

• Label the unlabeled Exercise 11.5.1 1/x continuity/integrability examples as (a)/(b).
• Attach Example 11.5.5 (a)–(e) docs to the piecewise-continuity claims.
• Drop a stray space in the Exercise 1.3.23 Lusin docstring.

Test plan

• CI build green

Made with Cursor

[teorth]

Holding this one — the Example 11.5.5 (a)–(e) labels and the Lusin docstring spacing fix are both fine, but the Exercise 11.5.1 (a)/(b) labels on the two 1/x examples are pointing at the wrong item, and would collide with a correct existing use.

Checking §11.5 against ch11.tex, the order is:

• Corollary 11.5.2 — continuous on [a,b] ⟹ Riemann integrable
• a remark: "Note that this Corollary is not true if [a,b] is replaced by any other sort of interval… For instance, the function f: (0,1) → R defined by f(x) := 1/x is continuous but not Riemann integrable."
• Proposition 11.5.3 — continuous and bounded ⟹ integrable
• Proposition 11.5.4 — piecewise continuous and bounded ⟹ integrable
• Exercise 11.5.1 = "Prove Proposition 11.5.4"
• Exercise 11.5.2 = f continuous non-negative with ∫ f = 0 ⟹ f = 0

So the two 1/x examples formalize the remark after Corollary 11.5.2, not Exercise 11.5.1. And Section_11_5.lean:216 already carries /-- Proposition 11.5.6 / Exercise 11.5.1 -/, which is the correct home for that exercise — so this PR would introduce a duplicate Exercise 11.5.1, which is the opposite of what the labelling pass is for.

Something like /-- Corollary 11.5.2 (sharpness) -/ on both, or a Remark-flavoured label, would fit better; your call on wording.

For the record, I made exactly this mistake myself in a PR I subsequently withdrew (#620) — I had labelled the same two examples Exercise 11.5.1 without checking. Sorry for any part that had in steering you toward it.

Drop the two Exercise 11.5.1 hunks and the rest is ready to go.