changelog, doc

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -69,6 +69,8 @@
 - in `measurable_realfun.v`:
   + lemmas `measurable_funN`
   + lemmas `nondecreasing_measurable`, `nonincreasing_measurable`
+- in `subspace_topology.v`:
+  + definition `from_subspace`
 
 ### Changed
 
@@ -83,6 +85,8 @@
 
 - in `lebesgue_integral_monotone_convergence.v`:
   + lemma `ge0_le_integral` (remove superfluous hypothesis)
+- in `subspace_topology.v`:
+  + notation `{within _, continuous _}` (now uses `from_subspace`)
 
 ### Renamed
 

theories/topology_theory/subspace_topology.v

@@ -9,16 +9,24 @@ From mathcomp Require Import product_topology.
 (* # Subspaces of topological spaces                                          *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*              subspace A == for (A : set T), this is a copy of T with a     *)
-(*                            topology that ignores points outside A          *)
-(*         incl_subspace x == with x of type subspace A with (A : set T),     *)
-(*                            inclusion of subspace A into T                  *)
-(*         nbhs_subspace x == filter associated with x : subspace A           *)
-(*          subspace_ent A == subspace entourages                             *)
-(*         subspace_ball A == balls of the pseudometric subspace structure    *)
-(*   continuousFunType A B == type of continuous function from set A to set B *)
-(*                            with domain subspace A                          *)
-(*                            The HB structure is ContinuousFun.              *)
+(*               subspace A == for (A : set T), this is a copy of T with a    *)
+(*                             topology that ignores points outside A         *)
+(*          incl_subspace x == with x of type subspace A with (A : set T),    *)
+(*                             inclusion of subspace A into T                 *)
+(*          nbhs_subspace x == filter associated with x : subspace A          *)
+(*        from_subspace A f == function of type `subspace A -> U` given a     *)
+(*                             function f of type `A -> U`                    *)
+(*                             The purpose of this definition is to preserve  *)
+(*                             the pretty-printing of the notation            *)
+(*                             {within _, continuous _} below. Its use is     *)
+(*                             however likely to be later superseded by a     *)
+(*                             better (compositional) mechanism.              *)
+(* {within A, continuous f} := continuous (from_subspace A f))                *)
+(*           subspace_ent A == subspace entourages                            *)
+(*          subspace_ball A == balls of the pseudometric subspace structure   *)
+(*    continuousFunType A B == type of continuous functions from set A to     *)
+(*                             set B with domain subspace A                   *)
+(*                             The HB structure is ContinuousFun.             *)
 (* ```                                                                        *)
 (******************************************************************************)