Skip to content

Commit

Permalink
fixing docs
Browse files Browse the repository at this point in the history
  • Loading branch information
@zstone1
zstone1 committed Sep 8, 2024
1 parent 15c7bc9 commit 365d578
Show file tree
Hide file tree
Showing 4 changed files with 26 additions and 18 deletions.
8 changes: 7 additions & 1 deletion CHANGELOG_UNRELEASED.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,8 +49,14 @@
+ definition `uniform_bounded`
+ theorem `Banach_Steinhauss`

### Changed
- in `topology.v`:
+ Structures `PointedFiltered`, `PointedNbhs`, `PointedUniform`,
`PseudoPointedMetric`

### Changed
- in `topology.v`:
+ removed the pointed assumptions from `FilteredType`, `Nbhs`,
`TopologicalType`, `UniformType`, and `PseudoMetricType`.
- in `normedtype.v`:
+ remove superflous parameters in lemmas `not_near_at_rightP` and `not_near_at_leftP`

Expand Down
6 changes: 0 additions & 6 deletions theories/cantor.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,12 +89,6 @@ Qed.
HB.instance Definition _ (U : Type) (T : U -> ptopologicalType) :=
Pointed.copy (forall x : U, T x) (prod_topology T).

Global Instance prod_topology_filter (U : Type) (T : U -> ptopologicalType) (f : prod_topology T) :
ProperFilter (nbhs f).
Proof.
exact: nbhs_pfilter.
Qed.

(**md**************************************************************************)
(* ## Part 1 *)
(* *)
Expand Down
7 changes: 7 additions & 0 deletions theories/function_spaces.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -398,6 +398,13 @@ by move=> z [w Uw] /inj <- //; rewrite inE.
Qed.

End product_embeddings.

Global Instance prod_topology_filter (U : Type) (T : U -> ptopologicalType) (f : prod_topology T) :
ProperFilter (nbhs f).
Proof.
exact: nbhs_pfilter.
Qed.

End product_spaces.

(**md the uniform topologies type *)
Expand Down
23 changes: 12 additions & 11 deletions theories/topology.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ Require Import reals signed.
(* 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 *)
(* ``` *)
(* *)
Expand Down Expand Up @@ -194,6 +195,7 @@ Require Import reals signed.
(* topologicalType == interface type for topological space *)
(* structure *)
(* the HB class is Topological. *)
(* ptopologicalType == a pointed topologicalType *)
(* open == set of open sets *)
(* open_nbhs p == set of open neighbourhoods of p *)
(* basis B == a family of open sets that converges *)
Expand All @@ -208,29 +210,27 @@ Require Import reals signed.
(* space from the properties of nbhs and *)
(* hence assumes that the carrier is a *)
(* filterType. *)
(* Pointed_isOpenTopological == factory for a topology defined by open *)
(* isOpenTopological == factory for a topology defined by open *)
(* sets *)
(* It builds the mixin for a topological *)
(* space from the properties of open *)
(* sets, assuming the carrier is a *)
(* pointed type. nbhs_of_open must be *)
(* used to declare a filterType. *)
(* Pointed_isBaseTopological == factory for a topology defined by a *)
(* sets, nbhs_of_open must be used to *)
(* declare a filterType. *)
(* isBaseTopological == factory for a topology defined by a *)
(* base of open sets *)
(* It builds the mixin for a topological *)
(* space from the properties of a base of *)
(* open sets; the type of indices must be *)
(* a pointedType, as well as the carrier. *)
(* a pointedType *)
(* 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 *)
(* Pointed_isSubBaseTopological == factory for a topology defined by a *)
(* isSubBaseTopological == factory for a topology defined by a *)
(* subbase of open sets *)
(* It builds the mixin for a topological *)
(* space from a subbase of open sets b *)
(* indexed on domain D; the type of *)
(* indices must be a pointedType. *)
(* indexed on domain D *)
(* *)
(* We endow several standard types with the structure of topology, e.g.: *)
(* - products `(T * U)%type` *)
Expand All @@ -239,11 +239,10 @@ Require Import reals signed.
(* *)
(* weak_topology f == weak topology by a function f : S -> T *)
(* on S *)
(* S must be a pointedType and T a *)
(* S must be a choiceType and T a *)
(* topologicalType. *)
(* sup_topology Tc == supremum topology of the family of *)
(* topologicalType structures Tc on T *)
(* T must be a pointedType. *)
(* quotient_topology Q == the quotient topology corresponding to *)
(* quotient Q : quotType T where T has *)
(* type topologicalType *)
Expand Down Expand Up @@ -294,6 +293,7 @@ Require Import reals signed.
(* uniformType == interface type for uniform spaces: a *)
(* type equipped with entourages *)
(* The HB class is Uniform. *)
(* puniformType == a pointed and uniform space *)
(* entourage == set of entourages in a uniform space *)
(* Nbhs_isUniform == factory to build a topological space *)
(* from a mixin for a uniform space *)
Expand All @@ -319,6 +319,7 @@ Require Import reals signed.
(* pseudoMetricType == interface type for pseudo metric space *)
(* structure: a type equipped with balls *)
(* The HB class is PseudoMetric. *)
(* pseudoPMetricType == a pointed an pseudoMetric space *)
(* ball x e == ball of center x and radius e *)
(* Nbhs_isPseudoMetric == factory to build a topological space *)
(* from a mixin for a pseudoMetric space *)
Expand Down

0 comments on commit 365d578

Please sign in to comment.