Skip to content

Commit

Permalink
fixes
Browse files Browse the repository at this point in the history 
- duplicated Reserved Notations
- duplicates in doc
- doc formatting
  • Loading branch information
@affeldt-aist
affeldt-aist committed Oct 1, 2024
1 parent e3a4e3f commit b808f3b
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 59 deletions.
22 changes: 12 additions & 10 deletions classical/filter.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,20 +4,23 @@ From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
From mathcomp Require Import archimedean.
From mathcomp Require Import boolp classical_sets functions wochoice.
From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.

(**md**************************************************************************)
(* # Filters *)
(* *)
(* The theory of (powerset) filters and tools for manipulating them. *)
(* This file introduces convergence for filters. It also provides the *)
(* interface of filtered types for associating a "canonical filter" to each *)
(* element. And lastly it provides typeclass instances for verifying when *)
(* a (set_system T) is really a filter in T, as a Filter or Properfilter *)
(* a (set_system T) is really a filter in T, as a Filter or Properfilter. *)
(* *)
(* Table of contents of the documentation: *)
(* Filters *)
(* - Structure of filter *)
(* - Theory of filters *)
(* - Near notations and tactics *)
(* + Notations *)
(* + Tactics *)
(* - Structure of filter *)
(* - Theory of filters *)
(* - Near notations and tactics *)
(* + Notations *)
(* + Tactics *)
(* *)
(* ## Structure of filter *)
(* ``` *)
(* filteredType U == interface type for types whose *)
Expand All @@ -28,7 +31,7 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
(* It extends Pointed. *)
(* nbhs p == set of sets associated to p (in a *)
(* filtered type) *)
(* pfilteredType U == a pointed and filtered type *)
(* pfilteredType U == a pointed and filtered type *)
(* hasNbhs == factory for filteredType *)
(* ``` *)
(* *)
Expand Down Expand Up @@ -160,7 +163,6 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
(* *)
(******************************************************************************)


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Expand Down Expand Up @@ -1611,4 +1613,4 @@ by rewrite AB0 in FAB.
Qed.

Lemma proper_meetsxx T (F : set_system T) (FF : ProperFilter F) : F `#` F.
Proof. by rewrite meetsxx; apply: filter_not_empty. Qed.
Proof. by rewrite meetsxx; apply: filter_not_empty. Qed.
61 changes: 12 additions & 49 deletions theories/topology.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,25 +8,19 @@ From mathcomp Require Import filter reals signed.
From mathcomp Require Export filter.

(**md**************************************************************************)
(* # Filters and basic topological notions *)
(* # Basic topological notions *)
(* *)
(* This file develops tools for the manipulation of basic topological *)
(* notions. The development of topological notions builds on "filtered types" *)
(* by extending the hierarchy. *)
(* *)
(* Basic topological notions *)
(* - Mathematical structures *)
(* + Topology *)
(* + Uniform spaces *)
(* + Pseudometric spaces *)
(* + Complete uniform spaces *)
(* + Complete pseudometric spaces *)
(* + Subspaces of topological spaces *)
(* *)
(******************************************************************************)

(**md**************************************************************************)
(* # Basic topological notions *)
(* Table of contents of the documentation: *)
(* - Topology *)
(* - Uniform spaces *)
(* - Pseudometric spaces *)
(* - Complete uniform spaces *)
(* - Complete pseudometric spaces *)
(* - Subspaces of topological spaces *)
(* *)
(* ## Mathematical structures *)
(* ### Topology *)
Expand Down Expand Up @@ -73,11 +67,12 @@ From mathcomp Require Export filter.
(* It builds the mixin for a topological *)
(* space from a subbase of open sets b *)
(* indexed on domain D *)
(* *)
(* ``` *)
(* We endow several standard types with the structure of topology, e.g.: *)
(* - products `(T * U)%type` *)
(* - matrices `'M[T]_(m, n)` *)
(* - natural numbers `nat` *)
(* ``` *)
(* \oo == "eventually" filter on nat: set of *)
(* predicates on natural numbers that are *)
(* eventually true *)
Expand Down Expand Up @@ -245,38 +240,6 @@ From mathcomp Require Export filter.
(* *)
(******************************************************************************)

Reserved Notation "{ 'near' x , P }" (at level 0, format "{ 'near' x , P }").
Reserved Notation "'\forall' x '\near' x_0 , P"
(at level 200, x name, P at level 200,
format "'\forall' x '\near' x_0 , P").
Reserved Notation "'\near' x , P"
(at level 200, x at level 99, P at level 200,
format "'\near' x , P", only parsing).
Reserved Notation "{ 'near' x & y , P }"
(at level 0, format "{ 'near' x & y , P }").
Reserved Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P"
(at level 200, x name, y name, P at level 200,
format "'\forall' x '\near' x_0 & y '\near' y_0 , P").
Reserved Notation "'\forall' x & y '\near' z , P"
(at level 200, x name, y name, P at level 200,
format "'\forall' x & y '\near' z , P").
Reserved Notation "'\near' x & y , P"
(at level 200, x, y at level 99, P at level 200,
format "'\near' x & y , P", only parsing).
(*Reserved Notation "[ 'filter' 'of' x ]" (format "[ 'filter' 'of' x ]").*)
Reserved Notation "F `=>` G" (at level 70, format "F `=>` G").
Reserved Notation "F --> G" (at level 70, format "F --> G").
Reserved Notation "[ 'lim' F 'in' T ]" (format "[ 'lim' F 'in' T ]").
Reserved Notation "[ 'cvg' F 'in' T ]" (format "[ 'cvg' F 'in' T ]").
Reserved Notation "x \is_near F" (at level 10, format "x \is_near F").
Reserved Notation "E @[ x --> F ]"
(at level 60, x name, format "E @[ x --> F ]").
Reserved Notation "E @[ x \oo ]"
(at level 60, x name, format "E @[ x \oo ]").
Reserved Notation "f @ F" (at level 60, format "f @ F").
Reserved Notation "E `@[ x --> F ]"
(at level 60, x name, format "E `@[ x --> F ]").
Reserved Notation "f `@ F" (at level 60, format "f `@ F").
Reserved Notation "A ^°" (at level 1, format "A ^°").
Reserved Notation "[ 'locally' P ]" (at level 0, format "[ 'locally' P ]").
Reserved Notation "x ^'" (at level 2, format "x ^'").
Expand Down Expand Up @@ -446,11 +409,11 @@ End Topological1.
#[global] Hint Extern 0 (ProperFilter (nbhs _)) =>
solve [apply: nbhs_pfilter] : typeclass_instances.

Global Instance alias_nbhs_filter {T : topologicalType} x :
Global Instance alias_nbhs_filter {T : topologicalType} x :
@Filter T^o (@nbhs T^o T x).
Proof. apply: @nbhs_filter T x. Qed.

Global Instance alias_nbhs_pfilter {T : topologicalType} x :
Global Instance alias_nbhs_pfilter {T : topologicalType} x :
@ProperFilter T^o (@nbhs T^o T x).
Proof. exact: @nbhs_pfilter T x. Qed.

Expand Down

0 comments on commit b808f3b

Please sign in to comment.