finalize changelog and doc

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -118,14 +118,6 @@
 - new files `signed_measure.v` and `radon_nikodym.v`
   + with the contents of `charge.v` (deprecated)
 
-- in `mathcomp_extra.v`:
-  + lemmas `divDl_ge0`, `divDl_le1`
-  + mixin `Zmodule_isSubNormed`
-  + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge)
-
-- in `unstable.v`:
-  + lemmas `divD_onem`
-
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:

CHANGELOG_UNRELEASED_new.md

@@ -0,0 +1,52 @@
+# Changelog (unreleased)
+
+## [Unreleased]
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + lemmas `divDl_ge0`, `divDl_le1`
+  + mixin `Zmodule_isSubNormed`
+  + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge)
+
+- in `unstable.v`:
+  + lemmas `divD_onem`
+
+- in `filter.v`:
+  + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType`
+
+- in `topology_structure.v`:
+  + structure `SubTopological`, notation `subTopologicalType`
+
+- in `tvs.v`:
+  + structure `SubConvexTvs`, notation `subConvexTvsType`
+
+- in `normed_module.v`:
+  + structure `SubNormedModule`, notation `subNormedModType`
+  + instance `ent_xsection_filter`
+  + factory `SubLmodule_isSubNormedmodule`
+
+- new file `hahn_banach_theorem.v`:
+  + module `LinearGraph`
+    * definitions `graph`, `linear_graph`
+    * lemmas `lingraph_00`, `lingraphZ`, `lingraphD`
+  + module `HahnBanachZorn`
+    * definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph`
+    * record `zorn_type`
+    * definition `zphi`
+    * lemma `zorn_type_eq`
+    * definition `zornS`
+    * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
+  + theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
+
+### Deprecated
+
+### Renamed
+
+### Generalized
+
+### Removed
+
+
+
+

classical/filter.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
 From mathcomp Require Import boolp classical_sets functions wochoice.
@@ -15,21 +15,31 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
 (*                                                                            *)
 (* ## Structure of filter                                                     *)
 (* ```                                                                        *)
-(*                   filteredType U == interface type for types whose         *)
-(*                                     elements represent sets of sets on U   *)
-(*                                     These sets are intended to be filters  *)
-(*                                     on U but this is not enforced yet.     *)
-(*                                     The HB class is called Filtered.       *)
-(*                                     It extends Pointed.                    *)
-(*                           nbhs p == set of sets associated to p (in a      *)
-(*                                     filtered type)                         *)
-(*                  pfilteredType U == a pointed and filtered type            *)
-(*                          hasNbhs == factory for filteredType               *)
+(*              filteredType U == interface type for types whose elements     *)
+(*                                represent sets of sets on U                 *)
+(*                                These sets are intended to be filters on U  *)
+(*                                but this is not enforced yet.               *)
+(*                                The HB class is called Filtered.            *)
+(*                                It extends Pointed.                         *)
+(*                      nbhs p == set of sets associated to p (in a filtered  *)
+(*                                type)                                       *)
+(*             pfilteredType U == a pointed and filtered type                 *)
+(*                     hasNbhs == factory for filteredType                    *)
+(*                    nbhsType == type of a structure that has a set system   *)
+(*                                of neighborhoods associated to each point   *)
+(*                   pnbhsType == same has nbhsType for pointed types         *)
 (*                     continuous f == f is continuous w.r.t the topology     *)
-(*                 filterI_iter F n == nth stage of recursively building the  *)
-(*                                     filter of finite intersections of F    *)
-(*                    finI_from D f == set of \bigcap_(i in E) f i where E is *)
-(*                                     a finite subset of D                   *)
+(*             isSubNbhs V S U == interface that states the continuity of val *)
+(*                                for U which has a subChoiceType and a       *)
+(*                                nbhsType                                    *)
+(*             subNbhsType V S == structure that extends a                    *)
+(*                                subChoiceType/nbhsType with the isSubNbhs   *)
+(*                                interface                                   *)
+(*                                The HB class is SubNbhs.                    *)
+(*            filterI_iter F n == nth stage of recursively building the       *)
+(*                                filter of finite intersections of F         *)
+(*               finI_from D f == set of \bigcap_(i in E) f i where E is a    *)
+(*                                a finite subset of D                        *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* We endow several standard types with the structure of filter, e.g.:        *)
@@ -951,6 +961,15 @@ Lemma continuous_comp (R S T : nbhsType) (f : R -> S) (g : S -> T) x :
   {for x, continuous (g \o f)}.
 Proof. exact: cvg_comp. Qed.
 
+HB.mixin Record isSubNbhs
+  (V : nbhsType) (S : pred V) U & SubChoice V S U & Nbhs U := {
+  continuous_valE : continuous (val : U -> V)
+}.
+
+#[short(type="subNbhsType")]
+HB.structure Definition SubNbhs (V : nbhsType) (S : pred V) :=
+  { U of SubChoice V S U & Nbhs U & isSubNbhs V S U}.
+
 Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) :
     {for x, continuous f} ->
   (\forall y \near f x, P y) -> (\near x, P (f x)).