fix: label Ex. 1.2.2' and Ex. 9.2.1 (a)–(d)

[Chessing234]

Summary

• Label the two halves of Exercise 1.2.2 as Exercise 1.2.2 / Exercise 1.2.2' (primed, not invented (i)/(ii)), matching 7a9e513.
• Add missing (a)–(d) docstrings on Exercise 9.2.1.
• Exercise 1.2.22 left to Measure theory 1.2.2: Exercises 1.2.18 and 1.2.22 have two parts, not three #632 ((iii) → (ii')).

Test plan

• CI Build book

[Chessing234]

@teorth gentle bump — this is a small Verso/docstring hygiene fix with green CI. Happy to rebase or adjust if anything looks off; otherwise ready whenever you have a moment.

[teorth]

Thanks for the careful work here — but I'm going to decline this one, because the premise doesn't hold for this repo.

Repeated identical exercise docstrings are intentional house style, not a build hazard. They appear throughout: 12x /-- Exercise 5.4.9 -/, 6x /-- Exercise 3.5.4 -/, 6x /-- Exercise 3.1.7 -/, and many more. There is no label or anchor machinery keyed on docstring text — literate.toml sets docstrings_as_text = true, so docstrings render as plain text and book anchors come from declaration names. The book has been building and deploying with these duplicates all along, which is also why CI is green on these PRs: there was nothing to fix.

The added parentheticals also introduce part-labels that aren't in the textbook (e.g. Definition 6.1.3 (ε-steady, def), Definition 6.1.8 (lim, characterization)), which risks reading as though the text has parts it doesn't.

If you'd like to propose changing this convention, please open an issue first — it should be settled repo-wide rather than section by section.

The contributions I'm most glad to receive are the ones you've been sending: corrections to sorryd statements that are false or mis-hypothesized, in the spirit of #517. Those have been genuinely valuable.

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

[teorth]

Could you rebase this on current main? It conflicts in Analysis/MeasureTheory/Section_1_2_2.lean, which has moved since (#574, #561, 874c8f3 and others touched the Exercise 1.2.x labels there) — worth checking whether the 1.2.22 hunk is still needed after that.

The Section 9.2 part is still wanted: Exercise_9_2_1c/d genuinely lack the docstrings that a/b have.

[Chessing234]

rebased onto main; dropped the 1.2.22 hunk (already labeled there) and kept the 1.2.2 split plus the missing 9.2.1 (c)/(d) docs.

[teorth]

One more thing to fold into the rebase — I checked both of these hunks against the measure theory text (measure.tex), and the part labels do not match it.

Exercise 1.2.22. This has since been labelled (i)/(ii)/(iii) on main by #574, so that hunk is now redundant. But the text has only two parts:

(i) If E ⊂ R^d and F ⊂ R^{d′}, show that (m^{d+d′})*(E × F) ≤ (m^d)*(E)(m^{d′})*(F) …
(ii) Let E ⊂ R^d, F ⊂ R^{d′} be Lebesgue measurable sets. Show that E × F is Lebesgue measurable, with m(E × F) = m(E) · m(F).

LebesgueMeasurable.prod and Lebesgue_measure.prod are the two halves of part (ii), so the third should be (ii') rather than (iii). I have opened #632 for that.

Exercise 1.2.2. The text has no lettered parts at all:

Give an example of a sequence of uniformly bounded, Riemann integrable functions f_n : [0,1] → R … that converge pointwise to a bounded function f : [0,1] → R that is not Riemann integrable. What happens if we replace pointwise convergence with uniform convergence?

Two questions, one exercise. Per the convention settled in 7a9e513 (primed variants rather than invented parts), these would be Exercise 1.2.2 and Exercise 1.2.2' — though the existing declaration name Ex_1_2_2b suggests the repo may already be thinking of them as (a)/(b), so worth a word from @teorth on which he prefers.

The Section 9.2 part of this PR is unaffected and still wanted.

[Chessing234]

switched 1.2.2 to the primed form (Exercise 1.2.2 / Exercise 1.2.2') per 7a9e513; left 1.2.22 to #632. 9.2.1 (a)–(d) unchanged.