Measure theory 1.2.2: restore Exercise 1.2.13 to the text's statement

[teorth]

Checked against An Introduction to Measure Theory, Exercise 1.2.13 (§1.2.2, p. 38):

We say that a sequence E_n of sets in R^d converges pointwise to another set E in R^d if the indicator functions 1_{E_n} converge pointwise to 1_E.
(i) Show that if the E_n are all Lebesgue measurable, and converge pointwise to E, then E is Lebesgue measurable also.
(ii) (Dominated convergence theorem) Suppose that the E_n are all contained in another Lebesgue measurable set F of finite measure. Show that m(E_n) converges to m(E).
(iii) Give a counterexample to show that the dominated convergence theorem fails if the E_n are not contained in a set of finite measure, even if we assume that the m(E_n) are all uniformly bounded.

So E is given, and the convergence is pointwise everywhere — not almost everywhere. The statements prior to #582 matched this exactly.

#582 recast the hypothesis as a.e. convergence and, in the process, moved E₀ out of the hypotheses and into the goal as an existential. That makes (i) and (ii) false:

Take E n = if Even n then ∅ else univ (resp. F). Each is measurable, but 1_{E_n}(x) oscillates 0,1,0,1 at every x, so the non-convergence set is everything — and IsNull is Lebesgue_outer_measure = 0. Hence no E₀ whatsoever satisfies the conclusion.

This restores the previous statements verbatim (the diff is byte-identical to the pre-#582 text, so it is known to build).

One remaining gap, not addressed here since it changes the difficulty of the exercise rather than fixing an error: part (iii) in the text also asks for the counterexample to have m(E_n) uniformly bounded, which the Lean statement does not require. Happy to add that in a follow-up if you would like it — E n = Icc n (n+1) in d = 1 satisfies it.