fix

CHANGELOG_UNRELEASED.md

@@ -4,55 +4,6 @@
 
 ### Added
 
-- in `kernel.v`:
-  + `kseries` is now an instance of `Kernel_isSFinite_subdef`
-- in `classical_sets.v`:
-  + lemma `setU_id2r`
-- in `lebesgue_measure.v`:
-  + lemma `compact_measurable`
-
-- in `measure.v`:
-  + lemmas `outer_measure_subadditive`, `outer_measureU2`
-
-- in `lebesgue_measure.v`:
-  + declare `lebesgue_measure` as a `SigmaFinite` instance
-  + lemma `lebesgue_regularity_inner_sup`
-- in `convex.v`:
-  + lemmas `conv_gt0`, `convRE`
-
-- in `exp.v`:
-  + lemmas `concave_ln`, `conjugate_powR`
-
-- in file `lebesgue_integral.v`,
-  + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and 
-    `lebesgue_differentiation_continuous`.
-
-- in `normedtype.v`:
-  + lemmas `open_itvoo_subset`, `open_itvcc_subset`
-
-- in `lebesgue_measure.v`:
-  + lemma `measurable_ball`
-
-- in file `normedtype.v`,
-  + new lemmas `normal_openP`, `uniform_regular`,
-    `regular_openP`, and `pseudometric_normal`.
-- in file `topology.v`,
-  + new definition `regular_space`.
-  + new lemma `ent_closure`.
-
-- in file `lebesgue_integral.v`,
-  + new lemmas `simple_bounded`, `measurable_bounded_integrable`, 
-    `compact_finite_measure`, `approximation_continuous_integrable`
-
-- in `sequences.v`:
-  + lemma `cvge_harmonic`
-
-- in `mathcomp_extra.v`:
-  + lemmas `le_bigmax_seq`, `bigmax_sup_seq`
-
-- in `constructive_ereal.v`:
-  + lemma `bigmaxe_fin_num`
-
 - in file `cantor.v`,
   + new definitions `cantor_space`, `cantor_like`, `pointedDiscrete`, and 
     `tree_of`.

theories/cantor.v

@@ -285,8 +285,7 @@ Let c_ind n (V : set T) (b : bool) :=
 Local Lemma cantor_map : exists f : cantor_space -> T,
   [/\ continuous f,
       set_surj [set: cantor_space] [set: T] f &
-      set_inj [set: cantor_space] f
-  ].
+      set_inj [set: cantor_space] f ].
 Proof.
 have [] := @tree_map_props
     (fun=> [topologicalType of bool]) T c_ind c_invar cmptT hsdfT.
@@ -390,14 +389,13 @@ Context (t0 t1 : T).
 Hypothesis T2e : t0 != t1.
 
 Local Lemma ent_balls' (E : set (T * T)) :
-  exists M : set (set T),
-    entourage E -> [/\
-      finite_set M,
-      forall A, M A -> exists a, A a /\
-        A `<=` closure [set y | split_ent E (a, y)],
-      exists A B : set T, M A /\ M B /\ A != B,
-      \bigcup_(A in M) A = [set: T] &
-      M `<=` closed].
+  exists M : set (set T), entourage E -> [/\
+    finite_set M,
+    forall A, M A -> exists a, A a /\
+      A `<=` closure [set y | split_ent E (a, y)],
+    exists A B : set T, M A /\ M B /\ A != B,
+    \bigcup_(A in M) A = [set: T] &
+    M `<=` closed].
 Proof.
 have [entE|?] := pselect (entourage E); last by exists point.
 move: cptT; rewrite compact_cover.