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

@@ -10,12 +10,12 @@ From HB Require Import structures.
 (*                                                                            *)
 (* This file develops the theory of the Cantor space, that is bool^nat with   *)
 (* the product topology. The two main theorems proved here are                *)
-(* homeomorphism_cantor_like, and cantor_surj, aka Alexandroff-Hausdorff.     *)
+(* homeomorphism_cantor_like, and cantor_surj, a.k.a. Alexandroff-Hausdorff.  *)
 (*                                                                            *)
-(*         cantor_space == the Cantor space, with its canonical metric        *)
+(*          cantor_space == the Cantor space, with its canonical metric       *)
 (*         cantor_like T == perfect + compact + hausdroff + zero dimensional  *)
-(*         pointed_discrete T == equips T with the discrete topology          *)
-(*         tree_of T == builds a topological tree with levels (T n)           *)
+(*    pointed_discrete T == equips T with the discrete topology               *)
+(*             tree_of T == builds a topological tree with levels (T n)       *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -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.
@@ -335,7 +334,7 @@ Lemma homeomorphism_cantor_like :
     continuous f /\
     (forall A, closed A -> closed (f @` A)).
 Proof.
-exists tree_map => /=.
+exists [the {splitbij _ >-> _} of tree_map] => /=.
 have [cts surj inje] := projT2 (cid cantor_map); split; first exact: cts.
 move=> A clA; apply: (compact_closed hsdfT).
 apply: (@continuous_compact _ _ tree_map); first exact: continuous_subspaceT.
@@ -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.