lemmas about Lebesgue's outer measure

[affeldt-aist]

Motivation for this change

Four lemmas about the Lebesgue measure.
The second one is actually the most interesting because we use to prove
an important corollary of the Vitali's theorem (PR to come)

• outer_measure_open_itv_cover:
  definition of the outer measure in terms of covers of open intervals
  (proposition 20 in Li)
• outer_measure_open:
  for a set A with bounded outer measure and an epsilon,
  there is an open that contains A and whose measure is
  less than the outer measure A + epsilon,
  (proposition 21 1) in Li)
• outer_measure_Gdelta:
  for a set A with bounded outer measure, there exists a G-delta sets
  that contains A and whose measure is the same as A
  (proposition 21 2) in Li)
• negligible_outer_measure:
  a set N is negligible for the lebesgue measure iff its outer measure is 0
  (corollary 22 in Li)

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[zstone1]

Look pretty good, just one comment on a slight generalization.

[zstone1]

Any reason not to phrase it as

(l^*)%mu A = ereal_inf [set (l^* A)%mu | open U /\ A `<=` U]

so it is more compatible with outer_measure_open_itv_cover's phrasing? It also has the benefit of being true in the unbounded case.

[affeldt-aist]

(l^*)%mu U = ereal_inf [set (l^* A)%mu | open U /\ A `<=` U] (note the typo fix)
has been added as a lemma to the last commit but I am not sure how to exploit it

in any case, it suggested that outer_measure_Gdelta and outer_measure_open_le (new name) do not need the boundedness hypothesis so it has been removed