From f6d0db4c408a3b029612dcd9f8061515be14d451 Mon Sep 17 00:00:00 2001 From: zstone Date: Sat, 26 Oct 2024 13:30:59 -0400 Subject: [PATCH] fixing some docs --- theories/topology_theory/subtype_topology.v | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/theories/topology_theory/subtype_topology.v b/theories/topology_theory/subtype_topology.v index 7f07f723a..a1a19eb38 100644 --- a/theories/topology_theory/subtype_topology.v +++ b/theories/topology_theory/subtype_topology.v @@ -7,16 +7,22 @@ From mathcomp Require Import product_topology subspace_topology. (**md**************************************************************************) (* # Subtypes of topological spaces *) (* We have two distinct ways of building topologies as subsets of a *) -(* topological space `X`. One is the `subspace topology`, which builds a new *) -(* topology on X which 'isolates' a set A. The other considers the sigma *) -(* type `set_type` in the weak topology by the inclusion. Note `subspace A` *) -(* has the advantage that it preserves all the algebraic structure on X, and *) -(* the relevant local behavior A (in particular, continuity). On the other *) -(* hand `set_val A` has the right global properties you'd expect for the *) -(* subset topology. But you can't easily add two elements of `set_val [0,1]`. *) +(* topological space `X`. One is the `subspace topology`, which is defined in *) +(* `subspace_topology.v`. It builds a topology on X which 'isolates' a set A. *) +(* Ther other, defined in this file, defines a topology on the sigma type *) +(* `set_type` in the weak topology by the inclusion. Note `subspace A` has *) +(* the advantage that it preserves all the algebraic structure on X, but only *) +(* the local behavior A (in particular, continuity). On the other hand *) +(* `set_type A` has the right global properties you'd expect for the subset *) +(* topology. But you can't easily add two elements of `set_val [0,1]`. *) (* Note the implicit coercion from sets to `set_val` from `classical`. *) (* *) (* This file provides `set_type` with a topology, and some theory. *) +(* ``` *) +(* sigT_of_setX == commutes `set_type` and product topologies *) +(* setX_of_sigT == commutes product and `set_type` topologies *) +(* ``` *) +(* *) (******************************************************************************) Local Open Scope classical_set_scope.