fixes

CHANGELOG_UNRELEASED.md

@@ -23,18 +23,6 @@
 - in `exp.v`:
   + lemmas `concave_ln`, `conjugate_powR`
 
-
-- in `lebesgue_measure.v`:
-  + lemma `measurable_mulrr`
-
-- in `constructive_ereal.v`:
-  + lemma `eqe_pdivr_mull`
-
-- new file `hoelder.v`:
-  + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]`
-  + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0`
-  + lemma `hoelder`
-
 - in file `lebesgue_integral.v`,
   + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and 
     `lebesgue_differentiation_continuous`.
@@ -51,8 +39,17 @@
 - in file `topology.v`,
   + new definition `regular_space`.
   + new lemma `ent_closure`.
+
+- in `lebesgue_measure.v`:
+  + lemma `measurable_mulrr`
+
+- in `constructive_ereal.v`:
+  + lemma `eqe_pdivr_mull`
+
 - new file `hoelder.v`:
-  + 
+  + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]`
+  + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0`
+  + lemma `hoelder`
 
 ### Changed
 

theories/lebesgue_integral.v

@@ -67,13 +67,6 @@ Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable").
 Reserved Notation "m1 '\x' m2" (at level 40, m2 at next level).
 Reserved Notation "m1 '\x^' m2" (at level 40, m2 at next level).
 
-Reserved Notation "'N[ mu ]_  p [ F ]"
-  (at level 5, F at level 36, mu at level 10,
-  format "'[' ''N[' mu ]_ p '/  ' [ F ] ']'").
-Reserved Notation "''N_' p [ F ]" (* for use as a local notation *)
-  (at level 5, F at level 36,
-  format "'[' ''N_' p '/  ' [ F ] ']'").
-
 #[global]
 Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core.