changelog, typo

CHANGELOG_UNRELEASED.md

@@ -2,6 +2,47 @@
 
 ## [Unreleased]
 
+added:
+
+- 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`
+
 ### Added
 
 - in file `cantor.v`,