From ff5c7432f861b7eabe263ad9b0119144f5ce14f5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 19 Jan 2023 05:33:44 +0900 Subject: [PATCH] fix changelog --- CHANGELOG_UNRELEASED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e236a259a..8d97c85a0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -126,6 +126,7 @@ to perform some tactics under a `\forall x \near F, ...` quantification. - in `normedtype.v`, added notations `^'+`, `^'-`, `+oo_R`, `-oo_R` - in `topology.v` + + definition `quotient_topology` + definition `quotient_topologicalType_mixin`, `quotient_topologicalType` + definition `quotient_open` + lemma `pi_continuous`, `quotient_continuous`,`repr_comp_continuous`