fix: label Example 11.5.5 / Cor. 11.5.2 sharpness; tidy Lusin docstring

[Chessing234]

Summary

• Part-label Example 11.5.5 (a)–(e)
• Label the two 1/x examples as Corollary 11.5.2 (sharpness) (a)/(b) — they formalize the remark after the corollary, not Exercise 11.5.1
• Tidy the Exercise 1.3.23 Lusin docstring spacing

Test plan

• CI build green

[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.

[Chessing234]

dropped the ex 11.5.1 labels on the 1/x examples and marked them as cor 11.5.2 sharpness instead; example 11.5.5 + lusin bits unchanged.