Measure theory 1.2.2: Exercises 1.2.18 and 1.2.22 have two parts, not three

[teorth]

Follow-up to #574, checked against An Introduction to Measure Theory.

Each of these exercises is split across three Lean declarations, and #574 labelled the third of each as part (iii). But in the text each has only two parts — it is part (ii) that carries two conclusions.

Exercise 1.2.18 (Inner measure), §1.2.2 p. 40:

(i) Show that this definition is well defined, i.e. that if A, A′ are two elementary sets containing E, that m(A) − m*(A\E) is equal to m(A′) − m*(A′\E).
(ii) Show that m_*(E) ≤ m*(E), and that equality holds if and only if E is Lebesgue measurable.

So inner_measure.le is the first half of (ii) and inner_measure.eq_iff is the second half.

Exercise 1.2.22, §1.2.2 p. 41:

(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 ⊂ R^{d+d′} is Lebesgue measurable, with m^{d+d′}(E × F) = m^d(E) · m^{d′}(F).

So LebesgueMeasurable.prod is the first half of (ii) and Lebesgue_measure.prod is the second half.

Relabelled both as (ii'), following the convention already chosen for Exercise 1.3.8(vi')/(vi'') in 7a9e513 — primed variants of the real part label, rather than inventing a part the text does not have.

I also checked Exercise 1.2.24 while I was here: it genuinely has four parts (i)–(iv) in the text, matching the equivalence relation, the complete metric, the closure statement, and the continuous extension. Its labels are correct and are left untouched.

Docstring-only change; no Lean code is touched.

[teorth]

Heads-up on interaction with #621, which spaces the Verso docstring closers in this same file: both PRs touch the Exercise 1.2.22(iii) line, so whichever lands second will need a one-line rebase.

I have made this branch's version the fully-correct end state — /-- Exercise 1.2.22(ii'"'"') (Product measure formula) -/, i.e. both the relabel and the closer space — so if there is a conflict, taking this side is the right resolution. The other two 1.2.22 closers in #621 are untouched here and unaffected.