changelog, typo

- format doc

CHANGELOG_UNRELEASED.md

@@ -13,8 +13,45 @@
 - in `lebesgue_integral.v`:
   + `sigma_finite_measure` instance on product measure `\x`
 
+- in `topology.v`:
+  + lemma `filter_bigI_within`
+  + lemma `near_powerset_map`
+  + lemma `near_powerset_map_monoE`
+  + lemma `fst_open`
+  + lemma `snd_open`
+  + definition `near_covering_within`
+  + lemma `near_covering_withinP`
+  + lemma `compact_setM`
+  + definition `regular`
+  + lemma `compact_regular`
+  + lemma `fam_compact_nbhs`
+  + definition `compact_open`, notation `{compact-open, U -> V}`
+  + notation `{compact-open, F --> f}`
+  + definition `compact_openK`
+  + definition `compact_openK_nbhs`
+  + instance `compact_openK_nbhs_filter`
+  + definition `compact_openK_topological_mixin`
+  + canonicals `compact_openK_filter`, `compact_openK_topological`,
+	`compact_open_pointedType`
+  + definition `compact_open_topologicalType`
+  + canonicals `compact_open_filtered`, `compact_open_topological`
+  + lemma `compact_open_cvgP`
+  + lemma `compact_open_open`
+  + lemma `compact_closedI`
+  + lemma `compact_open_fam_compactP`
+  + lemma `compact_equicontinuous`
+  + lemma `uniform_regular`
+  + lemma `continuous_curry`
+  + lemma `continuous_uncurry_regular`
+  + lemma `continuous_uncurry`
+  + lemma `curry_continuous`
+  + lemma `uncurry_continuous`
+
 ### Changed
-
+
+- in `topology.v`:
+  + lemma `pointwise_compact_cvg`
+
 ### Renamed
 
 ### Generalized