diff --git a/shell.nix b/shell.nix index c4bd94b28..48206c1f7 100644 --- a/shell.nix +++ b/shell.nix @@ -1,9 +1,9 @@ {withEmacs ? false, - nixpkgs ? (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/c4196cca9acd1c51f62baf10fcbe34373e330bb3.tar.gz"; - sha256 = "0jsisiw8yckq96r5rgdmkrl3a7y9vg9ivpw12h11m8w6rxsfn5m5"; + nixpkgs ? (fetchTarball { + url = "https://github.com/NixOS/nixpkgs/archive/82b54d490663b6d87b7b34b9cfc0985df8b49c7d.tar.gz"; + sha256 = "12gpsif48g5b4ys45x36g4vdf0srgal4c96351m7gd2jsgvdllyf"; }), -coq-version ? "default", +coq-version ? "8.10", print-env ? false }: with import nixpkgs {}; @@ -16,6 +16,7 @@ let "8.8" = coqPackages_8_8; "8.9" = coqPackages_8_9; "8.10" = coqPackages_8_10; + "8.11" = coqPackages_8_11; }."${coq-version}"; coq = myCoqPackages.coq; in @@ -23,8 +24,8 @@ stdenv.mkDerivation rec { name = "env"; env = buildEnv { name = name; paths = buildInputs; }; buildInputs = [ coq ] ++ (with myCoqPackages; - [mathcomp mathcomp-finmap mathcomp-bigenough - mathcomp-multinomials mathcomp-real-closed coqeal]) + [ mathcomp mathcomp-finmap mathcomp-bigenough + mathcomp-multinomials mathcomp-real-closed ]) ++ lib.optional withEmacs pgEmacs; shellHook = '' nixEnv (){ diff --git a/theories/boolp.v b/theories/boolp.v index 476504116..e05deb622 100644 --- a/theories/boolp.v +++ b/theories/boolp.v @@ -55,7 +55,6 @@ Proof. by case: extentionality=> _; apply. Qed. Lemma propeqE (P Q : Prop) : (P = Q) = (P <-> Q). Proof. by apply: propext; split=> [->|/propext]. Qed. - Lemma funeqE {T U : Type} (f g : T -> U) : (f = g) = (f =1 g). Proof. by rewrite propeqE; split=> [->//|/funext]. Qed. @@ -87,6 +86,9 @@ Proof. by rewrite propeqE; split=> [->//|?]; rewrite funeq3E=> ???; rewrite propeqE. Qed. +Lemma predext {T} (P Q : T -> Prop) : (forall x, P x <-> Q x) -> P = Q. +Proof. by rewrite predeqE. Qed. + Lemma propT (P : Prop) : P -> P = True. Proof. by move=> p; rewrite propeqE; tauto. Qed. @@ -276,7 +278,7 @@ move=> cb /asboolPn nb; apply/asboolPn. by apply: contra nb => /asboolP /cb /asboolP. Qed. -Definition contrapNN := contra. +Definition contrapNN := contrap. Lemma contrapL (Q P : Prop) : (Q -> ~ P) -> P -> ~ Q. Proof. diff --git a/theories/classical_sets.v b/theories/classical_sets.v index 51263846f..32631e3d2 100644 --- a/theories/classical_sets.v +++ b/theories/classical_sets.v @@ -96,6 +96,10 @@ Reserved Notation "[ 'set' x : T | P ]" (at level 0, x at level 99, only parsing). Reserved Notation "[ 'set' x | P ]" (at level 0, x, P at level 99, format "[ 'set' x | P ]"). +Reserved Notation "[ 'get' x : T | P ]" + (at level 0, x at level 99, only parsing). +Reserved Notation "[ 'get' x | P ]" + (at level 0, x, P at level 99, format "[ 'get' x | P ]"). Reserved Notation "[ 'set' E | x 'in' A ]" (at level 0, E, x at level 99, format "[ '[hv' 'set' E '/ ' | x 'in' A ] ']'"). Reserved Notation "[ 'set' E | x 'in' A & y 'in' B ]" @@ -315,11 +319,16 @@ Qed. Lemma subsetI A (X Y Z : set A) : (X `<=` Y `&` Z) = ((X `<=` Y) /\ (X `<=` Z)). Proof. -rewrite propeqE; split=> [H|[y z ??]]; split; by [move=> ?/H[]|apply y|apply z]. +rewrite propeqE; split=> [XYZ|[XY XZ] x Xx]; first by split=> x /XYZ[]. +by split; [apply: XY|apply: XZ]. Qed. Lemma subIset {A} (X Y Z : set A) : X `<=` Z \/ Y `<=` Z -> X `&` Y `<=` Z. -Proof. case => H a; by [move=> [/H] | move=> [_ /H]]. Qed. +Proof. by move=> [XZ x [/XZ]|YZ x [_ /YZ]]. Qed. + +Lemma subsetI2 (A : Type) (X Y X' Y' : set A) : + X `<=` X' -> Y `<=` Y' -> X `&` Y `<=` X' `&` Y'. +Proof. by move=> sX sY x [/sX ? /sY]. Qed. Lemma setD_eq0 A (X Y : set A) : (X `\` Y = set0) = (X `<=` Y). Proof. @@ -447,18 +456,18 @@ Record class_of (T : Type) := Class { Section ClassDef. -Structure type := Pack { sort; _ : class_of sort ; _ : Type }. +Structure type := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ := cT return class_of cT in c. +Definition class := let: Pack _ c := cT return class_of cT in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Local Coercion base : class_of >-> Choice.class_of. Definition pack m := - fun bT b of phant_id (Choice.class bT) b => @Pack T (Class b m) T. + fun bT b of phant_id (Choice.class bT) b => @Pack T (Class b m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. @@ -500,6 +509,8 @@ Canonical matrix_pointedType m n (T : pointedType) := PointedType 'M[T]_(m, n) (\matrix_(_, _) point)%R. Notation get := (xget point). +Notation "[ 'get' x : T | P ]" := (get [set x : T | P]) : classical_set_scope. +Notation "[ 'get' x | P ]" := [get x : _ | P] : classical_est_scope. Section PointedTheory. @@ -539,7 +550,7 @@ Hypothesis (Rsucc : forall s, exists t, R s t /\ s <> t /\ Let Teq := @gen_eqMixin T. Let Tch := @gen_choiceMixin T. -Let Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0) T. +Let Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0). Let lub := fun A : {A : set T | total_on A R} => get (fun t : Tp => (forall s, sval A s -> R s t) /\ forall r, (forall s, sval A s -> R s r) -> R t r). @@ -656,7 +667,7 @@ Lemma ZL_preorder T (t0 : T) (R : T -> T -> Prop) : exists t, premaximal R t. Proof. set Teq := @gen_eqMixin T; set Tch := @gen_choiceMixin T. -set Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0) T. +set Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0). move=> Rrefl Rtrans tot_max. set eqR := fun s t => R s t /\ R t s; set ceqR := fun s => [set t | eqR s t]. have eqR_trans r s t : eqR r s -> eqR s t -> eqR r t. diff --git a/theories/topology.v b/theories/topology.v index 682c96279..39101c81f 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -9,26 +9,26 @@ Require Import boolp Rstruct classical_sets posnum. (* topological notions. *) (* *) (* * Filters : *) -(* filteredType U == interface type for types whose *) +(* filterType 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. *) -(* FilteredType U T m == packs the function m: T -> set (set U) *) +(* FilterType U T m == packs the function m: T -> set (set U) *) (* to build a filtered type of type *) -(* filteredType U; T must have a *) +(* filterType U; T must have a *) (* pointedType structure. *) -(* [filteredType U of T for cT] == T-clone of the filteredType U *) +(* [filterType U of T for cT] == T-clone of the filterType U *) (* structure cT. *) -(* [filteredType U of T] == clone of a canonical filteredType U *) +(* [filterType U of T] == clone of a canonical filterType U *) (* structure on T. *) -(* Filtered.source Y Z == structure that records types X such *) +(* Filter.source Y Z == structure that records types X such *) (* that there is a function mapping *) (* functions of type X -> Y to filters on *) (* Z. Allows to infer the canonical *) (* filter associated to a function by *) (* looking at its source type. *) -(* Filtered.Source F == if F : (X -> Y) -> set (set Z), packs *) -(* X with F in a Filtered.source Y Z *) +(* Filter.Source F == if F : (X -> Y) -> set (set Z), packs *) +(* X with F in a Filter.source Y Z *) (* structure. *) (* locally p == set of sets associated to p (in a *) (* filtered type). *) @@ -46,7 +46,7 @@ Require Import boolp Rstruct classical_sets posnum. (* associated to F. *) (* [lim F in T] == limit in T of the canonical filter *) (* associated to F; T must have a *) -(* filteredType structure. *) +(* filterType structure. *) (* lim F == same as [lim F in T] where T is *) (* inferred from the type of the *) (* canonical filter associated to F. *) @@ -55,9 +55,9 @@ Require Import boolp Rstruct classical_sets posnum. (* cvg F <-> same as [cvg F in T] where T is *) (* inferred from the type of the *) (* canonical filter associated to F. *) -(* Filter F == type class proving that the set of *) +(* is_filter F == type class proving that the set of *) (* sets F is a filter. *) -(* ProperFilter F == type class proving that the set of *) +(* is_pfilter F == type class proving that the set of *) (* sets F is a proper filter. *) (* UltraFilter F == type class proving that the set of *) (* sets F is an ultrafilter *) @@ -69,7 +69,7 @@ Require Import boolp Rstruct classical_sets posnum. (* pfilter_on T == interface type for sets of sets on T *) (* that are proper filters. *) (* PFilterPack F FF == packs the set of sets F with the proof *) -(* FF of ProperFilter F to build a *) +(* FF of is_pfilter F to build a *) (* pfilter_on T structure. *) (* filtermap f F == image of the filter F by the function *) (* f. *) @@ -114,20 +114,20 @@ Require Import boolp Rstruct classical_sets posnum. (* \near x, P x := \forall y \near x, P x. *) (* {near F & G, P} == same as {near H, P}, where H is the *) (* product of the filters F and G. *) -(* \forall x \near F & y \near G, P x y := {near F & G, forall x y, P x y}. *) -(* \forall x & y \near F, P x y == same as before, with G = F. *) -(* \near x & y, P x y := \forall z \near x & t \near y, P x y. *) +(* \for x \near F & y \near G, P x y := {near F & G, forall x y, P x y}. *) +(* \for x & y \near F, P x y == same as before, with G = F. *) +(* \near x & y, P x y := \for z \near x & t \near y, P x y. *) (* x \is_near F == x belongs to a set P : in_filter F. *) (* --> Tactics: *) (* - near=> x introduces x: *) -(* On the goal \forall x \near F, G x, introduces the variable x and an *) +(* On the goal \for x \near F, G x, introduces the variable x and an *) (* "existential", and unaccessible hypothesis ?H x and asks the user to *) (* prove (G x) in this context. *) (* Under the hood delays the proof of F ?H and waits for near: x *) (* Also exists under the form near=> x y. *) (* - near: x discharges x: *) (* On the goal H_i x, and where x \is_near F, it asks the user to prove *) -(* that (\forall x \near F, H_i x), provided that H_i x does not depend *) +(* that (\for x \near F, H_i x), provided that H_i x does not depend *) (* on variables introduced after x. *) (* Under the hood, it refines by intersection the existential variable *) (* ?H attached to x, computes the intersection with F, and asks the *) @@ -148,7 +148,7 @@ Require Import boolp Rstruct classical_sets posnum. (* open sets. *) (* topologyOfFilterMixin loc_filt loc_sing loc_loc == builds the mixin for *) (* a topological space from the *) -(* properties of locally. *) +(* properties of nbhs. *) (* topologyOfOpenMixin opT opI op_bigU == builds the mixin for a *) (* topological space from the properties *) (* of open sets. *) @@ -162,7 +162,7 @@ Require Import boolp Rstruct classical_sets posnum. (* indices must be a pointedType. *) (* TopologicalType T m == packs the mixin m to build a *) (* topologicalType; T must have a *) -(* canonical filteredType T structure. *) +(* canonical filterType T structure. *) (* weak_topologicalType f == weak topology by f : S -> T on S; S *) (* must be a pointedType and T a *) (* topologicalType. *) @@ -178,7 +178,7 @@ Require Import boolp Rstruct classical_sets posnum. (* open == set of open sets. *) (* neigh p == set of open neighbourhoods of p. *) (* continuous f <-> f is continuous w.r.t the topology. *) -(* locally' x == set of neighbourhoods of x where x is *) +(* nbhs' x == set of neighbourhoods of x where x is *) (* excluded. *) (* closure A == closure of the set A. *) (* closed == set of closed sets. *) @@ -195,7 +195,7 @@ Require Import boolp Rstruct classical_sets posnum. (* product topology. *) (* *) (* * Uniform spaces : *) -(* locally_ ball == neighbourhoods defined using balls *) +(* nbhs_ ball == neighbourhoods defined using balls *) (* uniformType == interface type for uniform space *) (* structure. We use here a pseudo-metric *) (* definition of uniform space: a type *) @@ -203,7 +203,7 @@ Require Import boolp Rstruct classical_sets posnum. (* UniformMixin brefl bsym btriangle locb == builds the mixin for a *) (* uniform space from the properties of *) (* balls and the compatibility between *) -(* balls and locally. *) +(* balls and nbhs. *) (* UniformType T m == packs the uniform space mixin into a *) (* uniformType. T must have a canonical *) (* topologicalType structure. *) @@ -240,20 +240,20 @@ Require Import boolp Rstruct classical_sets posnum. (******************************************************************************) Reserved Notation "{ 'near' x , P }" (at level 0, format "{ 'near' x , P }"). -Reserved Notation "'\forall' x '\near' x_0 , P" +Reserved Notation "'\for' x '\near' x_0 , P" (at level 200, x ident, P at level 200, - format "'\forall' x '\near' x_0 , P"). + format "'\for' 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" +Reserved Notation "'\for' x '\near' x_0 & y '\near' y_0 , P" (at level 200, x ident, y ident, P at level 200, - format "'\forall' x '\near' x_0 & y '\near' y_0 , P"). -Reserved Notation "'\forall' x & y '\near' z , P" + format "'\for' x '\near' x_0 & y '\near' y_0 , P"). +Reserved Notation "'\for' x & y '\near' z , P" (at level 200, x ident, y ident, P at level 200, - format "'\forall' x & y '\near' z , P"). + format "'\for' 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). @@ -319,10 +319,7 @@ Canonical fct_lmodType U (R : ringType) (V : lmodType R) := Lemma fct_sumE (T : Type) (M : zmodType) n (f : 'I_n -> T -> M) (x : T) : (\sum_(i < n) f i) x = \sum_(i < n) f i x. -Proof. -elim: n f => [|n H] f; - by rewrite !(big_ord0,big_ord_recr) //= -[LHS]/(_ x + _ x) H. -Qed. +Proof. by elim/big_rec2: _ => // ? ? ? _ <-. Qed. End function_space. @@ -334,683 +331,794 @@ End Linear1. Section Linear2. Context (R : ringType) (U : lmodType R) (V : zmodType) (s : R -> V -> V) (s_law : GRing.Scale.law s). -Canonical linear_pointedType := PointedType {linear U -> V | GRing.Scale.op s_law} + Canonical linear_pointedType := PointedType {linear U -> V | GRing.Scale.op s_law} (@GRing.null_fun_linear R U V s s_law). End Linear2. -Module Filtered. - -(* Index a family of filters on a type, one for each element of the type *) -Definition locally_of U T := T -> set (set U). -Record class_of U T := Class { - base : Pointed.class_of T; - locally_op : locally_of U T +Structure nbhs_on T := Nbhs { + in_nbhs :> set (set T); +}. +Arguments Nbhs {T}. +Arguments in_nbhs : simpl never. + + +Notation "'\for' x '\near' x_0 , P" := (in_nbhs x_0 (fun x => P)) + (at level 200, x ident, P at level 200, format "'\for' x '\near' x_0 , P") : type_scope. +Notation "'\near' x , P" := (in_nbhs x (fun x => P)) + (at level 200, x at level 99, P at level 200, format "'\near' x , P", only parsing) : type_scope. + +Record is_filter {T : Type} (F : nbhs_on T) := IsFilter { + filterT_prop : \for x \near F, True; + filterI_prop : forall P Q : set T, + (\for x \near F, P x) -> (\for x \near F, Q x) -> + \for x \near F, P x /\ Q x; + filterS_prop : forall P Q : set T, P `<=` Q -> + (\for x \near F, P x) -> \for x \near F, Q x; }. -Section ClassDef. -Variable U : Type. - -Structure type := Pack { sort; _ : class_of U sort ; _ : Type }. -Local Coercion sort : type >-> Sortclass. -Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ := cT return class_of U cT in c. +Structure filter_on T := Filter { + in_filter :> set (set T); + _ : is_filter (Nbhs in_filter) +}. +Definition filter_class T (F : filter_on T) : is_filter (Nbhs (in_filter F)) := + let: Filter _ class := F in class. +Arguments Filter {T} _ _. +Canonical filter_nbhs_on T (F : filter_on T) := Eval hnf in + Nbhs (in_filter F). +Coercion filter_nbhs_on : filter_on >-> nbhs_on. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. -Notation xclass := (class : class_of U xT). -Local Coercion base : class_of >-> Pointed.class_of. -Definition pack m := - fun bT b of phant_id (Pointed.class bT) b => @Pack T (Class b m) T. +Lemma filter_is_filter (T : Type) (F : filter_on T) : is_filter F. +Proof. by case: F. Qed. -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition fpointedType := @Pointed.Pack cT xclass xT. +Lemma setT_is_filter (T : Type) : is_filter (Nbhs (@setT (set T))). +Proof. by constructor. Qed. -End ClassDef. +Definition setT_filter (T : Type) := Filter _ (setT_is_filter T). -(* filter on arrow sources *) -Structure source Z Y := Source { - source_type :> Type; - _ : (source_type -> Z) -> set (set Y) -}. -Definition source_filter Z Y (F : source Z Y) : (F -> Z) -> set (set Y) := - let: Source X f := F in f. +Section NearBasics. +Context {T : nonPropType}. +Implicit Type F : filter_on T. -Module Exports. -Coercion sort : type >-> Sortclass. -Coercion base : class_of >-> Pointed.class_of. -Coercion locally_op : class_of >-> locally_of. -Coercion eqType : type >-> Equality.type. -Canonical eqType. -Coercion choiceType : type >-> Choice.type. -Canonical choiceType. -Coercion fpointedType : type >-> Pointed.type. -Canonical fpointedType. -Notation filteredType := type. -Notation FilteredType U T m := (@pack U T m _ _ idfun). -Notation "[ 'filteredType' U 'of' T 'for' cT ]" := (@clone U T cT _ idfun) - (at level 0, format "[ 'filteredType' U 'of' T 'for' cT ]") : form_scope. -Notation "[ 'filteredType' U 'of' T ]" := (@clone U T _ _ id) - (at level 0, format "[ 'filteredType' U 'of' T ]") : form_scope. - -(* The default filter for an arbitrary element is the one obtained *) -(* from its type *) -Canonical default_arrow_filter Y (Z : pointedType) (X : source Z Y) := - FilteredType Y (X -> Z) (@source_filter _ _ X). -Canonical source_filter_filter Y := - @Source Prop _ (_ -> Prop) (fun x : (set (set Y)) => x). -Canonical source_filter_filter' Y := - @Source Prop _ (set _) (fun x : (set (set Y)) => x). +Lemma nearT F : \for x \near F, True. Proof. by case: F => ? []. Qed. -End Exports. -End Filtered. -Export Filtered.Exports. +Lemma nearI F P Q : (\for x \near F, P x) -> (\for x \near F, Q x) -> + \for x \near F, P x /\ Q x. +Proof. by case: F => ? [/= ? + ?]; apply. Qed. -Definition locally {U} {T : filteredType U} : T -> set (set U) := - Filtered.locally_op (Filtered.class T). -Arguments locally {U T} _ _ : simpl never. +Lemma nearS F P Q : P `<=` Q -> (\for x \near F, P x) -> \for x \near F, Q x. +Proof. by case: F => ? [/= ? ? +]; apply. Qed. -Definition filter_from {I T : Type} (D : set I) (B : I -> set T) : set (set T) := - [set P | exists2 i, D i & B i `<=` P]. +Lemma nearW F (P : set T) : (forall x : T, P x) -> (\for x \near F, P x). +Proof. by move=> Px; apply: nearS (nearT F). Qed. -(* the canonical filter on matrices on X is the product of the canonical filter - on X *) -Canonical matrix_filtered m n X (Z : filteredType X) : filteredType 'M[X]_(m, n) := - FilteredType 'M[X]_(m, n) 'M[Z]_(m, n) (fun mx => filter_from - [set P | forall i j, locally (mx i j) (P i j)] - (fun P => [set my : 'M[X]_(m, n) | forall i j, P i j (my i j)])). +End NearBasics. -Definition filter_prod {T U : Type} - (F : set (set T)) (G : set (set U)) : set (set (T * U)) := - filter_from (fun P => F P.1 /\ G P.2) (fun P => P.1 `*` P.2). +Definition filter_is_proper {T : Type} (F : nbhs_on T) := + ~ (\for x \near F, False). -Section Near. +Record is_pfilter {T : Type} (F : nbhs_on T) := IsPFilter { + filter_pfilter : is_filter F; + filter_not_empty_prop : filter_is_proper F; +}. +Coercion filter_pfilter : is_pfilter >-> is_filter. -Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). -Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). -Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). -Local Notation ph := (phantom _). +Structure pfilter_on T := PFilterPack { + in_pfilter :> set (set T); + _ : is_pfilter (Nbhs in_pfilter) +}. +Definition pfilter_class T (F : pfilter_on T) : is_pfilter (Nbhs F) := + let: PFilterPack _ class := F in class. +Arguments PFilterPack {T} _ _. +Canonical pfilter_nbhs_on T (F : pfilter_on T) := Eval hnf in Nbhs F. +Coercion pfilter_nbhs_on : pfilter_on >-> nbhs_on. +Canonical pfilter_filter_on T (F : pfilter_on T) := Eval hnf in + Filter F (pfilter_class F). +Coercion pfilter_filter_on : pfilter_on >-> filter_on. -Definition prop_near1 {X} {fX : filteredType X} (x : fX) - P (phP : ph {all1 P}) := locally x P. +Definition PFilter_of {T} (F : set (set T)) (fN0 : not (F set0)) := + fun (fF : filter_on T) of phant_id F (fF : set (set T)) => + fun fFF of phant_id (Filter _ fFF) fF => + PFilterPack F (IsPFilter fFF fN0). +Notation PFilter F fN0 := (@PFilter_of _ F fN0 _ id _ id). -Definition prop_near2 {X X'} {fX : filteredType X} {fX' : filteredType X'} - (x : fX) (x' : fX') := fun P of ph {all2 P} => - filter_prod (locally x) (locally x') (fun x => P x.1 x.2). +Identity Coercion set_id : set >-> Funclass. +Arguments filter : simpl never. -End Near. +(* Near Tactic *) -Notation "{ 'near' x , P }" := (@prop_near1 _ _ x _ (inPhantom P)) : type_scope. -Notation "'\forall' x '\near' x_0 , P" := {near x_0, forall x, P} : type_scope. -Notation "'\near' x , P" := (\forall x \near x, P) : type_scope. -Notation "{ 'near' x & y , P }" := - (@prop_near2 _ _ _ _ x y _ (inPhantom P)) : type_scope. -Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P" := - {near x_0 & y_0, forall x y, P} : type_scope. -Notation "'\forall' x & y '\near' z , P" := - {near z & z, forall x y, P} : type_scope. -Notation "'\near' x & y , P" := (\forall x \near x & y \near y, P) : type_scope. -Arguments prop_near1 : simpl never. -Arguments prop_near2 : simpl never. +Record filter_elt T (F : set (set T)) := FilterElt { + prop_filter_elt_proj : set T; + prop_filter_eltP_proj : F prop_filter_elt_proj +}. +(* add ball x e as a canonical instance of nbhs x *) + +Module Type FilterEltSig. +Axiom t : forall (T : Type) (F : set (set T)), filter_elt F -> T -> Prop. +Axiom tE : t = prop_filter_elt_proj. +End FilterEltSig. +Module FilterElt : FilterEltSig. +Definition t := prop_filter_elt_proj. +Lemma tE : t = prop_filter_elt_proj. Proof. by []. Qed. +End FilterElt. +(* Coercion FilterElt.t : filter_elt >-> Funclass. *) +Notation prop_of := FilterElt.t. +Definition prop_ofE := FilterElt.tE. +Notation "x \is_near F" := (@FilterElt.t _ F _ x). +Definition is_nearE := prop_ofE. -Lemma nearE {T} {F : set (set T)} (P : set T) : (\forall x \near F, P x) = F P. -Proof. by []. Qed. +Lemma prop_ofP T F (iF : @filter_elt T F) : F (prop_of iF). +Proof. by rewrite prop_ofE; apply: prop_filter_eltP_proj. Qed. -Definition filter_of X (fX : filteredType X) (x : fX) of phantom fX x := - locally x. -Notation "[ 'filter' 'of' x ]" := - (@filter_of _ _ _ (Phantom _ x)) : classical_set_scope. -Arguments filter_of _ _ _ _ _ /. +Definition filter_eltT T (F : filter_on T) : @filter_elt T F := + FilterElt (nearT _). +Canonical filter_eltI T (F : filter_on T) (P Q : @filter_elt T F) := + Eval hnf in FilterElt (nearI (prop_filter_eltP_proj P) (prop_filter_eltP_proj Q)). -Lemma filter_of_filterE {T : Type} (F : set (set T)) : [filter of F] = F. -Proof. by []. Qed. +Lemma filter_near_of T (F : filter_on T) + (P : @filter_elt T F) (Q : set T) : + (forall x, prop_of P x -> Q x) -> \for x \near F, Q x. +Proof. by move: P => [P FP] /=; rewrite prop_ofE /= => /nearS; apply. Qed. +(* Lemma filter_near_of T (F : {filter T}) *) +(* (P : @filter_elt T (nbhs F)) (Q : set T) : *) +(* (forall x, prop_of P x -> Q x) -> nbhs F Q. *) +(* Proof. by move: P => [P FP] /=; rewrite prop_ofE /= => /nearS; apply. Qed. *) -Lemma locally_filterE {T : Type} (F : set (set T)) : locally F = F. -Proof. by []. Qed. +Lemma near_acc_key : unit. Proof. exact: tt. Qed. -Module Export LocallyFilter. -Definition locally_simpl := (@filter_of_filterE, @locally_filterE). -End LocallyFilter. +Fact near_key : unit. Proof. exact. Qed. -Definition flim {T : Type} (F G : set (set T)) := G `<=` F. -Notation "F `=>` G" := (flim F G) : classical_set_scope. -Lemma flim_refl T (F : set (set T)) : F `=>` F. -Proof. exact. Qed. +Lemma mark_near (P : Prop) : locked_with near_key P -> P. +Proof. by rewrite unlock. Qed. -Lemma flim_trans T (G F H : set (set T)) : - (F `=>` G) -> (G `=>` H) -> (F `=>` H). -Proof. by move=> FG GH P /GH /FG. Qed. +Lemma near_acc T (F : filter_on T) (P : @filter_elt T F) (Q : set T) + (FQ : \for x \near F, Q x) : + locked_with near_key + (forall x, prop_of (filter_eltI P (FilterElt FQ)) x -> (Q x)). +Proof. by rewrite unlock => x /=; rewrite !prop_ofE /= => -[Px]. Qed. -Notation "F --> G" := (flim [filter of F] [filter of G]) : classical_set_scope. -Definition type_of_filter {T} (F : set (set T)) := T. +Lemma near_fork T (F : filter_on T) (P Q : @filter_elt T F) (G : set T) : + locked_with near_key (forall x, prop_of P x -> G x) -> + locked_with near_key (forall x, prop_of (filter_eltI P Q) x -> G x). +Proof. +rewrite !unlock => FG x /=; rewrite !prop_ofE /= => -[Px Qx]. +by have /= := FG x; apply; rewrite prop_ofE. +Qed. -Definition lim_in {U : Type} (T : filteredType U) := - fun F : set (set U) => get (fun l : T => F --> l). -Notation "[ 'lim' F 'in' T ]" := (@lim_in _ T [filter of F]) : classical_set_scope. -Notation lim F := [lim F in [filteredType _ of @type_of_filter _ [filter of F]]]. -Notation "[ 'cvg' F 'in' T ]" := (F --> [lim F in T]) : classical_set_scope. -Notation cvg F := [cvg F in [filteredType _ of @type_of_filter _ [filter of F]]]. +Tactic Notation "near=>" ident(x) := apply: filter_near_of => x ?. -Section FilteredTheory. +Ltac just_discharge_near x := + tryif match goal with Hx : x \is_near _ |- _ => move: (x) (Hx); apply: mark_near end + then idtac else fail "the variable" x "is not a ""near"" variable". +Ltac near_skip := + match goal with |- locked_with near_key (forall _, @FilterElt.t _ _ ?P _ -> _) => + tryif is_evar P then fail "nothing to skip" else apply: near_fork end. -Canonical filtered_prod X1 X2 (Z1 : filteredType X1) - (Z2 : filteredType X2) : filteredType (X1 * X2) := - FilteredType (X1 * X2) (Z1 * Z2) - (fun x => filter_prod (locally x.1) (locally x.2)). +Tactic Notation "near:" ident(x) := + just_discharge_near x; + tryif do ![apply: near_acc; [shelve|..]|near_skip] + then idtac + else fail "the goal depends on variables introduced after" x. -Lemma flim_prod T {U U' V V' : filteredType T} (x : U) (l : U') (y : V) (k : V') : - x --> l -> y --> k -> (x, y) --> (l, k). -Proof. -move=> xl yk X [[X1 X2] /= [HX1 HX2] H]; exists (X1, X2) => //=. -split; [exact: xl | exact: yk]. -Qed. +Ltac end_near := do ?exact: filter_eltT. -Lemma cvg_ex {U : Type} (T : filteredType U) (F : set (set U)) : - [cvg F in T] <-> (exists l : T, F --> l). -Proof. by split=> [cvg|/getPex//]; exists [lim F in T]. Qed. +Ltac done := + trivial; hnf; intros; solve + [ do ![solve [trivial | apply: sym_equal; trivial] + | discriminate | contradiction | split] + | case not_locked_false_eq_true; assumption + | match goal with H : ~ _ |- _ => solve [case H; trivial] end + | match goal with |- ?x \is_near _ => near: x; apply: prop_ofP end ]. -Lemma cvgP {U : Type} (T : filteredType U) (F : set (set U)) (l : T) : - F --> l -> [cvg F in T]. -Proof. by move=> Fl; apply/cvg_ex; exists l. Qed. +Canonical pfilter_on_eqType T := Eval hnf in EqType (pfilter_on T) gen_eqMixin. +Canonical pfilter_on_choiceType T := Eval hnf in + ChoiceType (pfilter_on T) gen_choiceMixin. -Lemma dvgP {U : Type} (T : filteredType U) (F : set (set U)) : - ~ [cvg F in T] -> [lim F in T] = point. -Proof. by rewrite /lim_in /=; case xgetP. Qed. +Definition pointfilter T (x : T) := [set A : set T | A x]. -(* CoInductive cvg_spec {U : Type} (T : filteredType U) (F : set (set U)) : *) -(* U -> Prop -> Type := *) -(* | HasLim of F --> [lim F in T] : cvg_spec T F [lim F in T] True *) -(* | HasNoLim of ~ [cvg F in U] : cvg_spec F point False. *) +Canonical pointfilter_nbhs T (x : T) := Eval hnf in + Nbhs (pointfilter x). -(* Lemma cvgP (F : set (set U)) : cvg_spec F (lim F) [cvg F in U]. *) -(* Proof. *) -(* have [cvg|dvg] := pselect [cvg F in U]. *) -(* by rewrite (propT cvg); apply: HasLim; rewrite -cvgE. *) -(* by rewrite (propF dvg) (dvgP _) //; apply: HasNoLim. *) -(* Qed. *) +Lemma pointfilter_is_filter T (x : T) : @is_filter T (Nbhs (pointfilter x)). +Proof. by split => //= P Q; apply. Qed. -End FilteredTheory. +Canonical pointfilter_filter T (x : T) := Eval hnf in + Filter (pointfilter x) (pointfilter_is_filter x). -Lemma locally_nearE {U} {T : filteredType U} (x : T) (P : set U) : - locally x P = \near x, P x. +Lemma pointfilterN0 T (x : T) : ~ [set A : set T | A x] set0. Proof. by []. Qed. -Lemma near_locally {U} {T : filteredType U} (x : T) (P : set U) : - (\forall x \near locally x, P x) = \near x, P x. -Proof. by []. Qed. +Canonical pointfilter_pfilter T (x : T) := Eval hnf in + PFilter (pointfilter x) (@pointfilterN0 _ x). -Lemma near2_curry {U V} (F : set (set U)) (G : set (set V)) (P : U -> set V) : - {near F & G, forall x y, P x y} = {near (F, G), forall x, P x.1 x.2}. -Proof. by []. Qed. +Lemma pfilter_is_filter (T : Type) (F : pfilter_on T) : + is_filter (Nbhs (in_pfilter F)). +Proof. by case: F => ? []. Qed. -Lemma near2_pair {U V} (F : set (set U)) (G : set (set V)) (P : set (U * V)) : - {near F & G, forall x y, P (x, y)} = {near (F, G), forall x, P x}. -Proof. by symmetry; congr (locally _); rewrite predeqE => -[]. Qed. +Lemma pfilter_on_pfilter (T : Type) (F : pfilter_on T) : + ~ (in_pfilter F) set0. +Proof. by case: F => ? []. Qed. -Definition near2E := (@near2_curry, @near2_pair). +Lemma pfilter_on_is_pfilter T (x : pfilter_on T) : is_pfilter x. +Proof. by case: x. Qed. -Lemma filter_of_nearI (X : Type) (fX : filteredType X) - (x : fX) (ph : phantom fX x) : forall P, - @filter_of X fX x ph P = @prop_near1 X fX x P (inPhantom (forall x, P x)). -Proof. by []. Qed. +Variant pfilter_spec T (F : set (set T)) : (set (set T)) -> Type := + PFilterSpec (p : pfilter_on T) & p = F :> set (set T) : pfilter_spec F p. -Module Export NearLocally. -Definition near_simpl := (@near_locally, @locally_nearE, filter_of_nearI). -Ltac near_simpl := rewrite ?near_simpl. -End NearLocally. +Lemma pfilterP T (F : nbhs_on T) : + is_pfilter (Nbhs F) -> pfilter_spec F F. +Proof. +move=> PF; rewrite -[in_nbhs F]/(in_nbhs (PFilterPack F PF)). +exact: PFilterSpec. +Qed. -Lemma near_swap {U V} (F : set (set U)) (G : set (set V)) (P : U -> set V) : - (\forall x \near F & y \near G, P x y) = (\forall y \near G & x \near F, P x y). +Lemma pfilterPW T (F : filter_on T) : (~ \near F, False) -> pfilter_spec F F. Proof. -rewrite propeqE; split => -[[/=A B] [FA FB] ABP]; -by exists (B, A) => // -[x y] [/=Bx Ay]; apply: (ABP (y, x)). +move=> PF; case: (@pfilterP _ F) => //. +by apply: IsPFilter => //; apply: filter_is_filter. Qed. -(** * Filters *) +Lemma near_ex_subproof {T : Type} (F : nbhs_on T) : + ~ in_nbhs F set0 -> (forall P, F P -> exists x, P x). +Proof. +move=> NFset0 P FP; apply: contrapNT NFset0 => nex; suff <- : P = set0 by []. +by rewrite funeqE => x; rewrite propeqE; split=> // Px; apply: nex; exists x. +Qed. -(** ** Definitions *) +Lemma filter_not_empty T (F : pfilter_on T) : ~ \near F, False. +Proof. by case: F => [? [/= ?]]; apply. Qed. +Arguments filter_not_empty {T} F _. -Class Filter {T : Type} (F : set (set T)) := { - filterT : F setT ; - filterI : forall P Q : set T, F P -> F Q -> F (P `&` Q) ; - filterS : forall P Q : set T, P `<=` Q -> F P -> F Q -}. -Global Hint Mode Filter - ! : typeclass_instances. +Definition near_ex {T : nonPropType} {F : pfilter_on T} : + forall P, in_nbhs F P -> exists x : T, P x := + near_ex_subproof (filter_not_empty F). -Class ProperFilter' {T : Type} (F : set (set T)) := { - filter_not_empty : not (F (fun _ => False)) ; - filter_filter' :> Filter F -}. -Global Hint Mode ProperFilter' - ! : typeclass_instances. -Arguments filter_not_empty {T} F {_}. +Lemma near_getP {T : pointedType} (F : pfilter_on T) (P : set T) : + in_nbhs F P -> P (get P). +Proof. by move=> /near_ex /getPex. Qed. -Notation ProperFilter := ProperFilter'. +Lemma near_const {T : nonPropType} (F : pfilter_on T) (P : Prop) : + (\for x \near F, P) -> P. +Proof. by move=> FP; case: (near_ex FP). Qed. +Arguments near_const {T} F P. -Lemma filter_setT (T' : Type) : Filter (@setT (set T')). -Proof. by constructor. Qed. +Tactic Notation "near" constr(F) "=>" ident(x) := + apply: (near_const F); near=> x. + +Definition nbhs_from {I T : Type} (D : set I) (B : I -> set T) : set (set T) := + [set P | exists2 i, D i & B i `<=` P]. -Lemma filterP_strong T (F : set (set T)) {FF : Filter F} (P : set T) : - (exists Q : set T, exists FQ : F Q, forall x : T, Q x -> P x) <-> F P. +Lemma nbhs_from_filter {I T : Type} (D : set I) (B : I -> set T) : + (exists i : I, D i) -> + (forall i j, D i -> D j -> exists2 k, D k & B k `<=` B i `&` B j) -> + is_filter (Nbhs (nbhs_from D B)). Proof. -split; last by exists P. -by move=> [Q [FQ QP]]; apply: (filterS QP). +move=> [i0 Di0] Binter; constructor; first by exists i0. +- move=> P Q [i Di BiP] [j Dj BjQ]; have [k Dk BkPQ]:= Binter _ _ Di Dj. + by exists k => // x /BkPQ [/BiP ? /BjQ]. +- by move=> P Q subPQ [i Di BiP]; exists i; apply: subset_trans subPQ. Qed. -Lemma filter_bigI T (I : choiceType) (D : {fset I}) (f : I -> set T) - (F : set (set T)) : - Filter F -> (forall i, i \in D -> F (f i)) -> - F (\bigcap_(i in [set i | i \in D]) f i). +Lemma nbhs_fromT_filter {I T : Type} (B : I -> set T) : + (exists _ : I, True) -> + (forall i j, exists k, B k `<=` B i `&` B j) -> + is_filter (Nbhs (nbhs_from setT B)). Proof. -move=> FF FfD. -suff: F [set p | forall i, i \in enum_fset D -> f i p] by []. -have {FfD} : forall i, i \in enum_fset D -> F (f i) by move=> ? /FfD. -elim: (enum_fset D) => [|i s ihs] FfD; first exact: filterS filterT. -apply: (@filterS _ _ _ (f i `&` [set p | forall i, i \in s -> f i p])). - by move=> p [fip fsp] j; rewrite inE => /orP [/eqP->|] //; apply: fsp. -apply: filterI; first by apply: FfD; rewrite inE eq_refl. -by apply: ihs => j sj; apply: FfD; rewrite inE sj orbC. +move=> [i0 _] BI; apply: nbhs_from_filter; first by exists i0. +by move=> i j _ _; have [k] := BI i j; exists k. Qed. -Structure filter_on T := FilterType { - filter :> (T -> Prop) -> Prop; - _ : Filter filter -}. -Definition filter_class T (F : filter_on T) : Filter F := - let: FilterType _ class := F in class. -Arguments FilterType {T} _ _. -Existing Instance filter_class. -(* Typeclasses Opaque filter. *) -Coercion filter_filter' : ProperFilter >-> Filter. - -Structure pfilter_on T := PFilterPack { - pfilter :> (T -> Prop) -> Prop; - _ : ProperFilter pfilter -}. -Definition pfilter_class T (F : pfilter_on T) : ProperFilter F := - let: PFilterPack _ class := F in class. -Arguments PFilterPack {T} _ _. -Existing Instance pfilter_class. -(* Typeclasses Opaque pfilter. *) -Canonical pfilter_filter_on T (F : pfilter_on T) := - FilterType F (pfilter_class F). -Coercion pfilter_filter_on : pfilter_on >-> filter_on. -Definition PFilterType {T} (F : (T -> Prop) -> Prop) - {fF : Filter F} (fN0 : not (F set0)) := - PFilterPack F (Build_ProperFilter' fN0 fF). -Arguments PFilterType {T} F {fF} fN0. - -Canonical filter_on_eqType T := EqType (filter_on T) gen_eqMixin. -Canonical filter_on_choiceType T := - ChoiceType (filter_on T) gen_choiceMixin. -Canonical filter_on_PointedType T := - PointedType (filter_on T) (FilterType _ (filter_setT T)). -Canonical filter_on_FilteredType T := - FilteredType T (filter_on T) (@filter T). - -Global Instance filter_on_Filter T (F : filter_on T) : Filter F. -Proof. by case: F. Qed. -Global Instance pfilter_on_ProperFilter T (F : pfilter_on T) : ProperFilter F. -Proof. by case: F. Qed. +Section ProdNbhsType. +Context {T U : Type}. -Lemma locally_filter_onE T (F : filter_on T) : locally F = locally (filter F). -Proof. by []. Qed. -Definition locally_simpl := (@locally_simpl, @locally_filter_onE). +Definition prod_nbhs (F : nbhs_on T) (G : nbhs_on U) := + nbhs_from (fun P => in_nbhs F P.1 /\ in_nbhs G P.2) (fun P => P.1 `*` P.2). -Lemma near_filter_onE T (F : filter_on T) (P : set T) : - (\forall x \near F, P x) = \forall x \near filter F, P x. -Proof. by []. Qed. -Definition near_simpl := (@near_simpl, @near_filter_onE). +Canonical prod_nbhs_nbhs F G := Eval hnf in Nbhs (prod_nbhs F G). -Program Definition trivial_filter_on T := FilterType [set setT : set T] _. -Next Obligation. -split=> // [_ _ -> ->|Q R sQR QT]; first by rewrite setIT. -by apply: eqEsubset => // ? _; apply/sQR; rewrite QT. +Lemma prod_nbhs_is_filter (F : filter_on T) (G : filter_on U) : + is_filter (Nbhs (prod_nbhs F G)). +Proof. +apply: nbhs_from_filter => [|[P Q] [P' Q'] /= [FP GQ] [FP' GQ']]. + by exists (setT, setT) => /=; split; apply: nearT. +exists (P `&` P', Q `&` Q') => /=; first by split; apply: nearI. +by move=> [p q] [/= [? ?] []]. Qed. -Canonical trivial_filter_on. + +Canonical prod_nbhs_filter F G := Eval hnf in + Filter _ (prod_nbhs_is_filter F G). -Lemma filter_locallyT {T : Type} (F : set (set T)) : - Filter F -> locally F setT. -Proof. by move=> FF; apply: filterT. Qed. -Hint Resolve filter_locallyT : core. +Lemma filter_prod_nontriv (F : pfilter_on T) (G : pfilter_on U) : + ~ \for x \near Nbhs (prod_nbhs F G), False. +Proof. +move=> [[/= X Y] [Xx Yx]]; rewrite subset0; apply/eqP; rewrite set0P. +near F => x1; near G => x2. +by exists (x1, x2); split => /=; [near: x1|near: x2]. +Grab Existential Variables. all: by end_near. Qed. -Lemma nearT {T : Type} (F : set (set T)) : Filter F -> \near F, True. -Proof. by move=> FF; apply: filterT. Qed. -Hint Resolve nearT : core. +Canonical prod_nbhs_pfilter F G := PFilter _ (@filter_prod_nontriv F G). -Lemma filter_not_empty_ex {T : Type} (F : set (set T)) : - (forall P, F P -> exists x, P x) -> ~ F set0. -Proof. by move=> /(_ set0) ex /ex []. Qed. +End ProdNbhsType. -Definition Build_ProperFilter {T : Type} (F : set (set T)) - (filter_ex : forall P, F P -> exists x, P x) - (filter_filter : Filter F) := - Build_ProperFilter' (filter_not_empty_ex filter_ex) (filter_filter). +Definition uncurry X Y Z (f : X -> Y -> Z) xy := f xy.1 xy.2. +Arguments uncurry : simpl never. -Lemma filter_ex_subproof {T : Type} (F : set (set T)) : - ~ F set0 -> (forall P, F P -> exists x, P x). -Proof. -move=> NFset0 P FP; apply: contrapNT NFset0 => nex; suff <- : P = set0 by []. -by rewrite funeqE => x; rewrite propeqE; split=> // Px; apply: nex; exists x. -Qed. +Definition uncurry_dep X Y Z (f : forall x : X, forall y : Y, Z x y) xy := + f xy.1 xy.2. +Arguments uncurry_dep : simpl never. -Definition filter_ex {T : Type} (F : set (set T)) {FF : ProperFilter F} := - filter_ex_subproof (filter_not_empty F). -Arguments filter_ex {T F FF _}. +Definition uncurry_sig X Y Z (f : forall x : X, forall y : Y x, Z x y) xy := + f (projT1 xy) (projT2 xy). +Arguments uncurry_sig : simpl never. -Lemma filter_getP {T : pointedType} (F : set (set T)) {FF : ProperFilter F} - (P : set T) : F P -> P (get P). -Proof. by move=> /filter_ex /getPex. Qed. +Notation "'\for' x '\near' x_0 & y '\near' y_0 , P" := + ((prod_nbhs x_0 y_0) (uncurry (fun x y => P))) + (at level 200, x ident, y ident, P at level 200, + format "'\for' x '\near' x_0 & y '\near' y_0 , P") : type_scope. +Notation "'\for' x & y '\near' z , P" := + (\for x \near z & y \near z, P) + (at level 200, x ident, y ident, P at level 200, + format "'\for' x & y '\near' z , P") : type_scope. +Notation "'\near' x & y , P" := (\for x \near x & y \near y, P) + (at level 200, x, y at level 99, P at level 200, format "'\near' x & y , P", only parsing) : type_scope. -(* Near Tactic *) +Section Near. -Record in_filter T (F : set (set T)) := InFilter { - prop_in_filter_proj : T -> Prop; - prop_in_filterP_proj : F prop_in_filter_proj -}. -(* add ball x e as a canonical instance of locally x *) - -Module Type PropInFilterSig. -Axiom t : forall (T : Type) (F : set (set T)), in_filter F -> T -> Prop. -Axiom tE : t = prop_in_filter_proj. -End PropInFilterSig. -Module PropInFilter : PropInFilterSig. -Definition t := prop_in_filter_proj. -Lemma tE : t = prop_in_filter_proj. Proof. by []. Qed. -End PropInFilter. -(* Coercion PropInFilter.t : in_filter >-> Funclass. *) -Notation prop_of := PropInFilter.t. -Definition prop_ofE := PropInFilter.tE. -Notation "x \is_near F" := (@PropInFilter.t _ F _ x). -Definition is_nearE := prop_ofE. +Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). +Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). +Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). +Local Notation ph := (phantom _). -Lemma prop_ofP T F (iF : @in_filter T F) : F (prop_of iF). -Proof. by rewrite prop_ofE; apply: prop_in_filterP_proj. Qed. +Definition prop_near1 {X} (F : nbhs_on X) P (phP : ph {all1 P}) := in_nbhs F P. -Definition in_filterT T F (FF : Filter F) : @in_filter T F := - InFilter (filterT). -Canonical in_filterI T F (FF : Filter F) (P Q : @in_filter T F) := - InFilter (filterI (prop_in_filterP_proj P) (prop_in_filterP_proj Q)). +Definition prop_near2 {X X'} (F : nbhs_on X) (F' : nbhs_on X') := + fun P of ph {all2 P} => prod_nbhs F F' (fun x => P x.1 x.2). -Lemma filter_near_of T F (P : @in_filter T F) (Q : set T) : Filter F -> - (forall x, prop_of P x -> Q x) -> F Q. -Proof. -by move: P => [P FP] FF /=; rewrite prop_ofE /= => /filterS; apply. -Qed. +End Near. -Fact near_key : unit. Proof. exact. Qed. +Notation "{ 'near' F , P }" := (@prop_near1 _ F _ (inPhantom P)) + (at level 0, format "{ 'near' F , P }") : type_scope. +Notation "{ 'near' F & G , P }" := (@prop_near2 _ _ F G _ (inPhantom P)) + (at level 0, format "{ 'near' F & G , P }") : type_scope. +Arguments prop_near1 : simpl never. +Arguments prop_near2 : simpl never. -Lemma mark_near (P : Prop) : locked_with near_key P -> P. -Proof. by rewrite unlock. Qed. +(* Lemma nbhsE {T : Type} {fT : nbhsType T} {F : fT} : nbhs F = F :> fT. *) +(* Proof. by []. Qed. *) -Lemma near_acc T F (P : @in_filter T F) (Q : set T) (FF : Filter F) - (FQ : \forall x \near F, Q x) : - locked_with near_key (forall x, prop_of (in_filterI FF P (InFilter FQ)) x -> Q x). -Proof. by rewrite unlock => x /=; rewrite !prop_ofE /= => -[Px]. Qed. +Lemma nbhs_setE {T : Type} (F : nbhs_on T) : in_nbhs F = F :> set (set T). +Proof. by []. Qed. -Lemma nearW T F (P Q : @in_filter T F) (G : set T) (FF : Filter F) : - locked_with near_key (forall x, prop_of P x -> G x) -> - locked_with near_key (forall x, prop_of (in_filterI FF P Q) x -> G x). +Lemma filter_setE {T : Type} (F : filter_on T) : in_nbhs F = F :> set (set T). +Proof. by []. Qed. + +Lemma pfilter_setE {T : Type} (F : pfilter_on T) : in_nbhs F = F :> set (set T). +Proof. by []. Qed. + +Lemma nbhsE {T : Type} (F : filter_on T) : Nbhs (in_nbhs F) = F. +Proof. by case: F. Qed. + +Canonical nbhs_on_any T (X : set (set T)) := Eval hnf in Nbhs X. +Canonical nbhs_nbhs_on_any T (X : set (set T)) := Eval hnf in Nbhs (in_nbhs (nbhs X)). + +Definition cvg_to {T : Type} {fT gT : nbhsType T} (F : fT) (G : gT) := nbhs G `<=` nbhs F. + +Notation "F --> G" := (cvg_to F G) + (at level 70, format "F --> G") : classical_set_scope. + +Lemma cvg_refl {T} {fT : nbhsType T} (F : fT) : F --> F. +Proof. exact. Qed. + +Lemma cvg_trans {T : Type} + {F G H : {nbhs T}} : +(* {fT gT hT : nbhsType T} (F : fT) (G : gT) (H : hT) : *) + (F --> G) -> (G --> H) -> (F --> H). +Proof. by move=> FG GH P /GH /FG. Qed. + +Definition type_of_nbhs {T} {fT : nbhsType T} (F : fT) := T. +Definition lim_in {U : Type} (fU1 fU2 : nbhsType U) (F : fU1) (phU2 : phant fU2) : fU2 := + [get l : fU2 | F --> l]. +Notation "[ 'lim' F 'in' T ]" := (@lim_in _ _ _ F (Phant T)) + (format "[ 'lim' F 'in' T ]") : classical_set_scope. +Notation lim F := [lim F in (type_of_nbhs F)]. +Notation "[ 'cvg' F 'in' T ]" := (F --> [lim F in T]) + (format "[ 'cvg' F 'in' T ]") : classical_set_scope. +Notation cvg F := [cvg F in (type_of_nbhs F)]. + +Section is_filteredTheory. + +Lemma cvg_prod {T} {fT1 fT2 fT3 fT4 : nbhsType T} (x : fT1) (y : fT2) (l : fT3) (k : fT4) : + x --> l -> y --> k -> (x, y) --> (l, k). Proof. -rewrite !unlock => FG x /=; rewrite !prop_ofE /= => -[Px Qx]. -by have /= := FG x; apply; rewrite prop_ofE. +move=> xl yk X [[X1 X2] /= [HX1 HX2] H]; exists (X1, X2) => //=. +by split; [exact: xl | exact: yk]. Qed. -Tactic Notation "near=>" ident(x) := apply: filter_near_of => x ?. +Lemma cvg_ex {U : Type} (fU1 fU2 : filterType U) (F : fU1) : + [cvg F in fU2] <-> (exists l : fU2, F --> l). +Proof. by split=> [cvg|/getPex//]; exists [lim F in _]. Qed. -Ltac just_discharge_near x := - tryif match goal with Hx : x \is_near _ |- _ => move: (x) (Hx); apply: mark_near end - then idtac else fail "the variable" x "is not a ""near"" variable". -Ltac near_skip := - match goal with |- locked_with near_key (forall _, @PropInFilter.t _ _ ?P _ -> _) => - tryif is_evar P then fail "nothing to skip" else apply: nearW end. +Lemma cvgP {U : Type} (fU1 fU2 : filterType U) (F : fU1) (l : fU2) : + F --> l -> [cvg F in fU2]. +Proof. by move=> Fl; apply/cvg_ex; exists l. Qed. -Tactic Notation "near:" ident(x) := - just_discharge_near x; - tryif do ![apply: near_acc; first shelve|near_skip] - then idtac - else fail "the goal depends on variables introduced after" x. +Lemma dvgP {U : Type} (fU1 fU2 : filterType U) (F : fU1) : + ~ [cvg F in fU2] -> [lim F in fU2] = point. +Proof. by rewrite /lim_in /=; case: xgetP. Qed. -Ltac end_near := do ?exact: in_filterT. +(* CoInductive cvg_spec {U : Type} (T : filterType U) (F : set (set U)) : *) +(* U -> Prop -> Type := *) +(* | HasLim of F --> [lim F in T] : cvg_spec T F [lim F in T] True *) +(* | HasNoLim of ~ [cvg F in U] : cvg_spec F point False. *) -Ltac done := - trivial; hnf; intros; solve - [ do ![solve [trivial | apply: sym_equal; trivial] - | discriminate | contradiction | split] - | case not_locked_false_eq_true; assumption - | match goal with H : ~ _ |- _ => solve [case H; trivial] end - | match goal with |- ?x \is_near _ => near: x; apply: prop_ofP end ]. +(* Lemma cvgP (F : set (set U)) : cvg_spec F (lim F) [cvg F in U]. *) +(* Proof. *) +(* have [cvg|dvg] := pselect [cvg F in U]. *) +(* by rewrite (propT cvg); apply: HasLim; rewrite -cvgE. *) +(* by rewrite (propF dvg) (dvgP _) //; apply: HasNoLim. *) +(* Qed. *) -Lemma have_near (U : Type) (fT : filteredType U) (x : fT) (P : Prop) : - ProperFilter (locally x) -> (\forall x \near x, P) -> P. -Proof. by move=> FF nP; have [] := @filter_ex _ _ FF (fun=> P). Qed. -Arguments have_near {U fT} x. +End is_filteredTheory. -Tactic Notation "near" constr(F) "=>" ident(x) := - apply: (have_near F); near=> x. +Lemma near2_curry {U V} {fU : nbhsType U} {fV : nbhsType V} + (F : fU) (G : fV) (P : U -> set V) : + {near F & G, forall x y, P x y} = {near (F, G), forall x, P x.1 x.2}. +Proof. by []. Qed. -Lemma near T (F : set (set T)) P (FP : F P) (x : T) - (Px : prop_of (InFilter FP) x) : P x. +Lemma near2_pair {U V} (F : {filter U}) (G : {filter V}) (P : set (U * V)) : + {near F & G, forall x y, P (x, y)} = {near (F, G), forall x, P x}. +Proof. by rewrite near2_curry; congr {near _, _}; rewrite predeqE => -[]. Qed. + +Definition near2E := (@near2_curry, @near2_pair). + +Lemma near_swap {U V} (F : {filter U}) (G : {filter V}) (P : U -> set V) : + (\for x \near F & y \near G, P x y) = (\for y \near G & x \near F, P x y). +Proof. +rewrite propeqE; split => -[[/=A B] [FA FB] ABP]; +by exists (B, A) => // -[x y] [/=Bx Ay]; apply: (ABP (y, x)). +Qed. + +Lemma filter_not_empty_ex {T : Type} (F : set (set T)) : + (forall P, F P -> exists x, P x) -> ~ \near F, False. +Proof. by move=> /(_ set0) ex /ex []. Qed. + +Definition Build_is_pfilter {T : Type} (F : set (set T)) + (near_ex : forall P, F P -> exists x, P x) + (filter_filter : is_filter (nbhs F)) := + Build_is_pfilter' (filter_filter) (filter_not_empty_ex near_ex). + +Lemma filter_bigI {T} {fT : filterType T} (I : choiceType) + (D : {fset I}) (f : I -> set T) (F : fT) : + (forall i, i \in D -> nbhs F (f i)) -> + nbhs F (\bigcap_(i in [set i | i \in D]) f i). +Proof. +move=> FfD. +suff: nbhs F [set p | forall i, i \in enum_fset D -> f i p] by []. +have {FfD} : forall i, i \in enum_fset D -> nbhs F (f i) by move=> ? /FfD. +elim: (enum_fset D) => [|i s ihs] FfD; first exact: nearS (nearT _). +apply: (@nearS _ _ _ (f i `&` [set p | forall i, i \in s -> f i p])). + by move=> p [fip fsp] j; rewrite inE => /orP [/eqP->|] //; apply: fsp. +apply: nearI; first by apply: FfD; rewrite inE eq_refl. +by apply: ihs => j sj; apply: FfD; rewrite inE sj orbC. +Qed. + +Lemma near {T} {fT : nbhsType T} {F : fT} P (FP : nbhs F P) (x : T) + (Px : prop_of (FilterElt FP) x) : P x. Proof. by move: Px; rewrite prop_ofE. Qed. -Arguments near {T F P} FP x Px. +Arguments near {T fT F P} FP x Px. -Lemma filterE {T : Type} {F : set (set T)} : - Filter F -> forall P : set T, (forall x, P x) -> F P. -Proof. by move=> ???; near=> x => //. Unshelve. end_near. Qed. -Lemma filter_app (T : Type) (F : set (set T)) : - Filter F -> forall P Q : set T, F (fun x => P x -> Q x) -> F P -> F Q. -Proof. by move=> FF P Q subPQ FP; near=> x; suff: P x; near: x. +Section NearTheorems. +Context {T : Type} {fT : filterType T}. +Implicit Type (F : fT). + +Lemma near_all {x : fT} {P : set T} : (forall x, P x) -> \near x, P x. +Proof. by move=> ?; near=> x0. Unshelve. end_near. Qed. + +Lemma near_app {F} (P Q : set T) : + (\for x \near F, P x -> Q x) -> (nbhs F) P -> (nbhs F) Q. +Proof. by move=> subPQ FP; near=> x; suff: P x; near: x. Grab Existential Variables. by end_near. Qed. -Lemma filter_app2 (T : Type) (F : set (set T)) : - Filter F -> forall P Q R : set T, F (fun x => P x -> Q x -> R x) -> - F P -> F Q -> F R. -Proof. by move=> ???? PQR FP; apply: filter_app; apply: filter_app FP. Qed. +Lemma near_app2 {F} : + forall P Q R : set T, nbhs F (fun x => P x -> Q x -> R x) -> + nbhs F P -> nbhs F Q -> nbhs F R. +Proof. by move=> ? ? ? PQR FP; apply: near_app; apply: near_app FP. Qed. -Lemma filter_app3 (T : Type) (F : set (set T)) : - Filter F -> forall P Q R S : set T, F (fun x => P x -> Q x -> R x -> S x) -> - F P -> F Q -> F R -> F S. -Proof. by move=> ????? PQR FP; apply: filter_app2; apply: filter_app FP. Qed. +Lemma near_app3 {F} : + forall P Q R S : set T, nbhs F (fun x => P x -> Q x -> R x -> S x) -> + nbhs F P -> nbhs F Q -> nbhs F R -> nbhs F S. +Proof. by move=> ? ? ? ? PQR FP; apply: near_app2; apply: near_app FP. Qed. -Lemma filterS2 (T : Type) (F : set (set T)) : - Filter F -> forall P Q R : set T, (forall x, P x -> Q x -> R x) -> - F P -> F Q -> F R. -Proof. by move=> ? ? ? ? ?; apply: filter_app2; apply: filterE. Qed. +Lemma nearS2 {F} : + forall P Q R : set T, (forall x, P x -> Q x -> R x) -> + nbhs F P -> nbhs F Q -> nbhs F R. +Proof. by move=> ? ? ? ?; apply/near_app2/near_all. Qed. -Lemma filterS3 (T : Type) (F : set (set T)) : - Filter F -> forall P Q R S : set T, (forall x, P x -> Q x -> R x -> S x) -> - F P -> F Q -> F R -> F S. -Proof. by move=> ? ? ? ? ? ?; apply: filter_app3; apply: filterE. Qed. +Lemma nearS3 {F} : + forall P Q R S : set T, (forall x, P x -> Q x -> R x -> S x) -> + nbhs F P -> nbhs F Q -> nbhs F R -> nbhs F S. +Proof. by move=> ? ? ? ? ?; apply/near_app3/near_all. Qed. -Lemma filter_const {T : Type} {F} {FF: @ProperFilter T F} (P : Prop) : - F (fun=> P) -> P. -Proof. by move=> FP; case: (filter_ex FP). Qed. +End NearTheorems. +Arguments near_all {T fT x P}. -Lemma in_filter_from {I T : Type} (D : set I) (B : I -> set T) (i : I) : - D i -> filter_from D B (B i). -Proof. by exists i. Qed. +Section Near2Theorems. +Context {I T U : nonPropType} {fT : filterType T} {fU : filterType U}. +Implicit Type (F : fT). -Lemma near_andP {T : Type} F (b1 b2 : T -> Prop) : Filter F -> - (\forall x \near F, b1 x /\ b2 x) <-> - (\forall x \near F, b1 x) /\ (\forall x \near F, b2 x). +Lemma near_andP {F} (b1 b2 : T -> Prop) : + (\for x \near F, b1 x /\ b2 x) <-> + (\for x \near F, b1 x) /\ (\for x \near F, b2 x). Proof. -move=> FF; split=> [H|[H1 H2]]; first by split; apply: filterS H => ? []. -by apply: filterS2 H1 H2. +split=> [H|[H1 H2]]; first by split; move: H; apply: nearS => ? []. +by apply: nearS2 H1 H2. Qed. -Lemma nearP_dep {T U} {F : set (set T)} {G : set (set U)} - {FF : Filter F} {FG : Filter G} (P : T -> U -> Prop) : - (\forall x \near F & y \near G, P x y) -> - \forall x \near F, \forall y \near G, P x y. +Lemma nearP_dep {F : fT} {G : fU} (P : T -> U -> Prop) : + (\for x \near F & y \near G, P x y) -> + \for x \near F, \for y \near G, P x y. Proof. move=> [[Q R] [/=FQ GR]] QRP. -by apply: filterS FQ => x Q1x; apply: filterS GR => y Q2y; apply: (QRP (_, _)). +by apply: nearS FQ => x Q1x; apply: nearS GR => y Q2y; apply: (QRP (_, _)). Qed. -Lemma filter2P T U (F : set (set T)) (G : set (set U)) - {FF : Filter F} {FG : Filter G} (P : set (T * U)) : - (exists2 Q : set T * set U, F Q.1 /\ G Q.2 +Lemma near2P (F : fT) (G : fU) (P : set (T * U)) : + (exists2 Q : set T * set U, nbhs F Q.1 /\ nbhs G Q.2 & forall (x : T) (y : U), Q.1 x -> Q.2 y -> P (x, y)) - <-> \forall x \near (F, G), P x. + <-> \for x \near (F, G), P x. Proof. split=> [][[A B] /=[FA GB] ABP]; exists (A, B) => //=. by move=> [a b] [/=Aa Bb]; apply: ABP. by move=> a b Aa Bb; apply: (ABP (_, _)). Qed. -Lemma filter_ex2 {T U : Type} (F : set (set T)) (G : set (set U)) - {FF : ProperFilter F} {FG : ProperFilter G} (P : set T) (Q : set U) : - F P -> G Q -> exists x : T, exists2 y : U, P x & Q y. -Proof. by move=> /filter_ex [x Px] /filter_ex [y Qy]; exists x, y. Qed. -Arguments filter_ex2 {T U F G FF FG _ _}. - -Lemma filter_fromP {I T : Type} (D : set I) (B : I -> set T) (F : set (set T)) : - Filter F -> F `=>` filter_from D B <-> forall i, D i -> F (B i). -Proof. -split; first by move=> FB i ?; apply/FB/in_filter_from. -by move=> FB P [i Di BjP]; apply: (filterS BjP); apply: FB. -Qed. - -Lemma filter_fromTP {I T : Type} (B : I -> set T) (F : set (set T)) : - Filter F -> F `=>` filter_from setT B <-> forall i, F (B i). -Proof. by move=> FF; rewrite filter_fromP; split=> [P i|P i _]; apply: P. Qed. +Lemma in_nbhs_from (D : set I) (B : I -> set T) (i : I) : + D i -> nbhs_from D B (B i). +Proof. by exists i. Qed. -Lemma filter_from_filter {I T : Type} (D : set I) (B : I -> set T) : - (exists i : I, D i) -> - (forall i j, D i -> D j -> exists2 k, D k & B k `<=` B i `&` B j) -> - Filter (filter_from D B). +Lemma nbhs_fromP (D : set I) (B : I -> set T) (F : fT) : + F --> nbhs_from D B <-> forall i, D i -> nbhs F (B i). Proof. -move=> [i0 Di0] Binter; constructor; first by exists i0. -- move=> P Q [i Di BiP] [j Dj BjQ]; have [k Dk BkPQ]:= Binter _ _ Di Dj. - by exists k => // x /BkPQ [/BiP ? /BjQ]. -- by move=> P Q subPQ [i Di BiP]; exists i; apply: subset_trans subPQ. +split; first by move=> FB i ?; apply/FB/in_nbhs_from. +by move=> FB P [i Di BjP]; apply: (nearS BjP); apply: FB. Qed. -Lemma filter_fromT_filter {I T : Type} (B : I -> set T) : - (exists _ : I, True) -> - (forall i j, exists k, B k `<=` B i `&` B j) -> - Filter (filter_from setT B). -Proof. -move=> [i0 _] BI; apply: filter_from_filter; first by exists i0. -by move=> i j _ _; have [k] := BI i j; exists k. -Qed. +Lemma nbhs_fromTP (B : I -> set T) (F : fT) : + F --> nbhs_from setT B <-> forall i, nbhs F (B i). +Proof. by rewrite nbhs_fromP; split=> [P i|P i _]; apply: P. Qed. -Lemma filter_from_proper {I T : Type} (D : set I) (B : I -> set T) : - Filter (filter_from D B) -> +Lemma nbhs_from_proper (D : set I) (B : I -> set T) : + is_filter (nbhs (nbhs_from D B)) -> (forall i, D i -> B i !=set0) -> - ProperFilter (filter_from D B). + is_pfilter (nbhs_from D B). Proof. -move=> FF BN0; apply: Build_ProperFilter=> P [i Di BiP]. +move=> FF BN0; apply: Build_is_pfilter => // P [i Di BiP]. by have [x Bix] := BN0 _ Di; exists x; apply: BiP. Qed. +End Near2Theorems. + +Lemma near_ex2 {T U : nonPropType} {fT : pfilterType T} {fU : pfilterType U} + (F : fT) (G : fU) (P : set T) (Q : set U) : + nbhs F P -> nbhs G Q -> exists x : T, exists2 y : U, P x & Q y. +Proof. by move=> /near_ex [x Px] /near_ex [y Qy]; exists x, y. Qed. + (** ** Limits expressed with filters *) +Module NonIdFun. +Section Ctx. +Context {U V : Type}. + +Structure call_of (condition : unit) (result : bool) := Call {callee : U -> V}. +Definition maybeId (f : U -> V) := tt. +Definition call f := Call (maybeId f) false f. + +Structure test_of (result : bool) := Test {condition :> unit}. +Definition test_negative := Test false tt. + +Structure type (phUV : phant (U -> V)) := + Check {result : bool; test : test_of result; frame : call_of test result}. +Definition check result test frame := @Check (Phant (U -> V)) result test frame. +End Ctx. +Definition test_id U := Test true (maybeId (@id U)). + +Module Exports. +Canonical call. +Canonical test_id. +Canonical test_negative. +Canonical check. +Notation nonIdFun T := (@type _ _ (Phant T)). +Coercion callee : call_of >-> Funclass. +Coercion frame : type >-> call_of. +Notation notId f := (@check false test_negative (@call _ _ f)). +End Exports. + +End NonIdFun. +Export NonIdFun.Exports. + Definition filtermap {T U : Type} (f : T -> U) (F : set (set T)) := [set P | F (f @^-1` P)]. -Arguments filtermap _ _ _ _ _ /. +Canonical filtermap_nbhs T (fT : nbhsType T) U (f : T -> U) (F : fT) := Eval hnf in + Nbhs (filtermap f (nbhs F)). -Lemma filtermapE {U V : Type} (f : U -> V) - (F : set (set U)) (P : set V) : filtermap f F P = F (f @^-1` P). +Definition mkfun {T T'} (f : forall x : T, T') := fun x => f x. +Arguments mkfun _ _ _ /. + +Notation "f @ F" := (filtermap f (in_nbhs (nbhs F))) + (at level 60, format "f @ F") : classical_set_scope. +Notation "E @[ x --> F ]" := (filtermap (mkfun (fun x => E)) (in_nbhs (nbhs F))) + (at level 60, x ident, format "E @[ x --> F ]") : classical_set_scope. + +Lemma near_map {U V : Type} {fU : nbhsType U} (f : nonIdFun (U -> V)) + (F : fU) (P : set V) : nbhs (f @ F) P = \for x \near F, P (f x). Proof. by []. Qed. -Notation "E @[ x --> F ]" := - (filtermap (fun x => E) [filter of F]) : classical_set_scope. -Notation "f @ F" := (filtermap f [filter of F]) : classical_set_scope. -Global Instance filtermap_filter T U (f : T -> U) (F : set (set T)) : - Filter F -> Filter (f @ F). +Lemma filtermap_is_filter T (fT : filterType T) U (f : T -> U) (F : fT) : is_filter (nbhs (f @ F)). Proof. -move=> FF; constructor => [|P Q|P Q PQ]; rewrite ?filtermapE ?filter_ofE //=. -- exact: filterT. -- exact: filterI. -- by apply: filterS=> ?/PQ. +constructor => [|P Q|P Q PQ]; rewrite ?near_map ?filter_ofE //=. +- exact: nearT. +- exact: nearI. +- by apply: nearS=> ?/PQ. Qed. -Typeclasses Opaque filtermap. -Global Instance filtermap_proper_filter T U (f : T -> U) (F : set (set T)) : - ProperFilter F -> ProperFilter (f @ F). -Proof. -move=> FF; apply: Build_ProperFilter'; -by rewrite filtermapE; apply: filter_not_empty. -Qed. -Definition filtermap_proper_filter' := filtermap_proper_filter. +Canonical filtermap_filter T (fT : filterType T) U (f : T -> U) (F : fT) := Eval hnf in + Filter (filtermap f (nbhs F)) (filtermap_is_filter f F). -Definition filtermapi {T U : Type} (f : T -> set U) (F : set (set T)) := - [set P | \forall x \near F, exists y, f x y /\ P y]. +Lemma filtermap_is_not_empty {T : Type} (fT : pfilterType T) {U : Type} + (f : T -> U) (F : fT) : ~ \for _ \near f @ F, False. +Proof. by rewrite near_map; apply: filter_not_empty. Qed. +Arguments filtermap_is_not_empty {T fT U} f F. -Notation "E `@[ x --> F ]" := - (filtermapi (fun x => E) [filter of F]) : classical_set_scope. -Notation "f `@ F" := (filtermapi f [filter of F]) : classical_set_scope. +Canonical filtermap_pfilter {T : pointedType} U (f : T -> U) (F : {pfilter T}) := Eval hnf in + PFilter (filtermap f (nbhs F)) (filtermap_is_not_empty f F). -Lemma filtermapiE {U V : Type} (f : U -> set V) - (F : set (set U)) (P : set V) : - filtermapi f F P = \forall x \near F, exists y, f x y /\ P y. +Fact filtermapi_key : unit. Proof. exact: tt. Qed. +Definition filtermapi {T U : Type} (f : T -> set U) (F : set (set T)) : set (set U) := + [set P | \for x \near F, exists y, f x y /\ P y]. +Canonical filtermapi_nbhs {T U} {fT : nbhsType T} (f : T -> U -> Prop) (F : fT) : nbhs_on U := Eval hnf in + Nbhs (filtermapi f (nbhs F)). + +Notation "E `@[ x --> y ]" := (filtermapi (fun x => E) (in_nbhs (nbhs y))) + (at level 60, x ident, format "E `@[ x --> y ]") : classical_set_scope. +Notation "f `@ x" := (filtermapi f (in_nbhs (nbhs x))) + (at level 60, format "f `@ x") : classical_set_scope. + +Lemma near_mapi {U} {fU : nbhsType U} {V : Type} (f : U -> set V) + (F : fU) (P : set V) : + nbhs (f `@ F) P = \for x \near F, exists y, f x y /\ P y. Proof. by []. Qed. -Global Instance filtermapi_filter T U (f : T -> set U) (F : set (set T)) : - infer {near F, is_totalfun f} -> Filter F -> Filter (f `@ F). +Definition nearE := (@near_map, @near_mapi). + +Lemma filtermapi_is_filter {T U} {fT : filterType T} (f : T -> set U) (F : fT) : + {near F, is_totalfun f} -> is_filter (nbhs (f `@ F)). Proof. -move=> f_totalfun FF; rewrite /filtermapi; apply: Build_Filter. (* bug *) -- by apply: filterS f_totalfun => x [[y Hy] H]; exists y. -- move=> P Q FP FQ; near=> x. +move=> f_totalfun; apply: Build_is_filter. (* bug *) +- by rewrite nearE; apply: nearS f_totalfun => x [[y Hy] H]; exists y. +- move=> P Q; rewrite !nearE => FP FQ; near=> x. have [//|y [fxy Py]] := near FP x. have [//|z [fxz Qz]] := near FQ x. have [//|_ fx_prop] := near f_totalfun x. by exists y; split => //; split => //; rewrite [y](fx_prop _ z). -- move=> P Q subPQ FP; near=> x. +- move=> P Q subPQ; rewrite !nearE => FP; near=> x. by have [//|y [fxy /subPQ Qy]] := near FP x; exists y. Grab Existential Variables. all: end_near. Qed. -Typeclasses Opaque filtermapi. +Lemma near_map2 {T T' U U'} {fT : filterType T} {fT' : filterType T'} + (f : T -> U) (g : T' -> U') + (F : fT) (G : fT') (P : U -> set U') : + (\for y \near f @ F & y' \near g @ G, P y y') = + (\for x \near F & x' \near G , P (f x) (g x')). +Proof. +rewrite propeqE; split=> -[[A B] /= [fFA fGB] ABP]. + rewrite !nearE in fFA fGB. + exists (f @^-1` A, g @^-1` B) => //= -[x y /=] xyAB. + by apply: (ABP (_, _)); apply: xyAB. +exists (f @` A, g @` B) => //=; last first. + by move=> -[a1 a2] [/= [x Ax <-] [x' Bx' <-]]; apply: (ABP (_, _)). +rewrite !nearE; split; first by apply: nearS fFA=> x Ax; exists x. +by apply: nearS fGB => x Bx; exists x. +Qed. + +Lemma complete_fun_subproof + {T : Type} {pfT : pfilterType T} {U : choiceType} (F : pfT) + (f : T -> U -> Prop) : {near F, is_totalfun f} -> + {g : T -> U | \for t \near F, f t = eq (g t)}. +Proof. +move=> fF; suff: exists g, `[<\for t \near F, f t = eq (g t)>]. + by move=> /sigW[g]; exists g; apply/asboolP. +have [x0 [[y0 fxy0 fx0P]]] := near_ex fF. +exists (fun x => xget y0 (f x)); apply/asboolP; near=> t. +rewrite predeqE => u; have [|[v ftv] ftP]// := near fF t. +by case: xgetP => [x -> ftx|/(_ v)//]; split=> [/(ftP _ _ ftx)|<-]. +Grab Existential Variables. all: end_near. Qed. + +Definition complete_fun + {T : Type} {pfT : pfilterType T} {U : choiceType} (F : pfT) + (f : T -> U -> Prop) (fFtotal : {near F, is_totalfun f}) : T -> U + := projT1 (complete_fun_subproof fFtotal). + +Definition complete_funE + {T : Type} {pfT : pfilterType T} {U : choiceType} (F : pfT) + (f : T -> U -> Prop) (fFtotal : {near F, is_totalfun f}) : + \for t \near F, f t = eq (complete_fun fFtotal t) + := projT2 (complete_fun_subproof fFtotal). + +Lemma nbhseqE T (F G : {nbhs T}) : + (nbhs F = nbhs G :> set _) = (forall P, nbhs F P <-> nbhs G P). +Proof. by rewrite predeqE propeqE; split => []. Qed. -Global Instance filtermapi_proper_filter - T U (f : T -> U -> Prop) (F : set (set T)) : - infer {near F, is_totalfun f} -> - ProperFilter F -> ProperFilter (f `@ F). +Lemma nbhs_on_eqE {T} (F G : {nbhs T}) : + (F = G) = (forall P, nbhs F P <-> nbhs G P). Proof. -move=> f_totalfun FF; apply: Build_ProperFilter. -by move=> P; rewrite /filtermapi => /filter_ex [x [y [??]]]; exists y. +rewrite -nbhseqE; apply/propext => //=; split => [->//|]. +by case: F G => [F] [G]/= eqFG; rewrite [F]eqFG. Qed. -Definition filter_map_proper_filter' := filtermapi_proper_filter. -Lemma flim_id T (F : set (set T)) : x @[x --> F] --> F. -Proof. exact. Qed. -Arguments flim_id {T F}. +Lemma filtermapi_complete + {T : Type} {pfT : pfilterType T} {U : choiceType} (F : pfT) + (f : T -> U -> Prop) (fFtotal : {near F, is_totalfun f}) : + f `@ F = complete_fun fFtotal @ F. +Proof. +rewrite predeqE; split; rewrite !nearE => Fx /=; near=> t. + have [//|u [ftu xu]] := near Fx t. + by move: ftu; rewrite (near (complete_funE fFtotal) t)// => ->. +exists (complete_fun fFtotal t); split; last by near: t. +by rewrite (near (complete_funE fFtotal) t). +Grab Existential Variables. all: end_near. Qed. + +Lemma filtermapi_proper_filter + {T U : pointedType} (f : T -> U -> Prop) (F : {pfilter T}) : + {near F, is_totalfun f} -> is_pfilter (f `@ F). +Proof. +move=> fFtotal; rewrite (filtermapi_complete fFtotal). +exact: pfilter_on_is_pfilter. +Qed. + +Section CvgTheory. +Context {T U V : Type} {fT : filterType T}. -Lemma appfilter U V (f : U -> V) (F : set (set U)) : - f @ F = [set P : set _ | \forall x \near F, P (f x)]. +Lemma cvg_id (y : set (set T)) : id @ y --> y. Proof. by []. Qed. -Lemma flim_app U V (F G : set (set U)) (f : U -> V) : +Lemma cvg_app (F G : set (set U)) (f : U -> V) : F --> G -> f @ F --> f @ G. Proof. by move=> FG P /=; exact: FG. Qed. -Lemma flimi_app U V (F G : set (set U)) (f : U -> set V) : +Lemma cvgi_app (F G : set (set U)) (f : U -> set V) : F --> G -> f `@ F --> f `@ G. -Proof. by move=> FG P /=; exact: FG. Qed. +Proof. by move=> FG P; rewrite !nearE; exact: FG. Qed. -Lemma flim_comp T U V (f : T -> U) (g : U -> V) +Lemma cvg_comp (f : T -> U) (g : U -> V) (F : set (set T)) (G : set (set U)) (H : set (set V)) : - f @ F `=>` G -> g @ G `=>` H -> g \o f @ F `=>` H. -Proof. by move=> fFG gGH; apply: flim_trans gGH => P /fFG. Qed. + f @ F --> G -> g @ G --> H -> g \o f @ F --> H. +Proof. +move=> fFG gGH; apply: cvg_trans gGH => P; rewrite !nearE. +by move=> /fFG; rewrite nearE. +Qed. -Lemma flimi_comp T U V (f : T -> U) (g : U -> set V) +Lemma cvgi_comp (f : T -> U) (g : U -> set V) (F : set (set T)) (G : set (set U)) (H : set (set V)) : - f @ F `=>` G -> g `@ G `=>` H -> g \o f `@ F `=>` H. -Proof. by move=> fFG gGH; apply: flim_trans gGH => P /fFG. Qed. + f @ F --> G -> g `@ G --> H -> g \o f `@ F --> H. +Proof. +move=> fFG gGH; apply: cvg_trans gGH => P. +by rewrite nearE => /fFG; rewrite !nearE. +Qed. -Lemma flim_eq_loc {T U} {F : set (set T)} {FF : Filter F} (f g : T -> U) : - {near F, f =1 g} -> g @ F `=>` f @ F. -Proof. by move=> eq_fg P /=; apply: filterS2 eq_fg => x <-. Qed. +Lemma cvg_eq_loc {F : fT} (f g : T -> U) : + {near F, f =1 g} -> g @ F --> f @ F. +Proof. by move=> eq_fg P /=; rewrite !nearE; apply: nearS2 eq_fg => x/= <-. Qed. -Lemma flimi_eq_loc {T U} {F : set (set T)} {FF : Filter F} (f g : T -> set U) : - {near F, f =2 g} -> g `@ F `=>` f `@ F. +Lemma cvgi_eq_loc {F : fT} (f g : T -> set U) : + {near F, f =2 g} -> g `@ F --> f `@ F. Proof. -move=> eq_fg P /=; apply: filterS2 eq_fg => x eq_fg [y [fxy Py]]. +move=> eq_fg P /=; rewrite !nearE; apply: nearS2 eq_fg => x eq_fg [y [fxy Py]]. by exists y; rewrite -eq_fg. Qed. +End CvgTheory. + (** ** Specific filters *) Section at_point. @@ -1019,233 +1127,201 @@ Context {T : Type}. Definition at_point (a : T) (P : set T) : Prop := P a. -Global Instance at_point_filter (a : T) : ProperFilter (at_point a). +Lemma at_point_filter (a : T) : is_pfilter (at_point a). Proof. by constructor=> //; constructor=> // P Q subPQ /subPQ. Qed. -Typeclasses Opaque at_point. End at_point. -(** Filters for pairs *) +(** is_filters for pairs *) -Global Instance filter_prod_filter T U (F : set (set T)) (G : set (set U)) : - Filter F -> Filter G -> Filter (filter_prod F G). +Lemma filter_prod1 {T U} {F : {filter T}} {G : {filter U}} (P : set T) : + (\for x \near F, P x) -> \for x \near F & _ \near G, P x. Proof. -move=> FF FG; apply: filter_from_filter. - by exists (setT, setT); split; apply: filterT. -move=> [P Q] [P' Q'] /= [FP GQ] [FP' GQ']. -exists (P `&` P', Q `&` Q') => /=; first by split; apply: filterI. -by move=> [x y] [/= [??] []]. +move=> FP; exists (P, setT)=> //= [|[? ? []//]]. +by split=> //; apply: nearT. Qed. -Canonical prod_filter_on T U (F : filter_on T) (G : filter_on U) := - FilterType (filter_prod F G) (filter_prod_filter _ _). - -Global Instance filter_prod_proper {T1 T2 : Type} - {F : (T1 -> Prop) -> Prop} {G : (T2 -> Prop) -> Prop} - {FF : ProperFilter F} {FG : ProperFilter G} : - ProperFilter (filter_prod F G). +Lemma filter_prod2 {T U} {F : {filter T}} {G : {filter U}} (P : set U) : + (\for y \near G, P y) -> \for _ \near F & y \near G, P y. Proof. -apply: filter_from_proper => -[A B] [/=FA GB]. -by have [[x ?] [y ?]] := (filter_ex FA, filter_ex GB); exists (x, y). +move=> FP; exists (setT, P)=> //= [|[? ? []//]]. +by split=> //; apply: nearT. Qed. -Definition filter_prod_proper' := @filter_prod_proper. -Lemma filter_prod1 {T U} {F : set (set T)} {G : set (set U)} - {FG : Filter G} (P : set T) : - (\forall x \near F, P x) -> \forall x \near F & _ \near G, P x. -Proof. -move=> FP; exists (P, setT)=> //= [|[?? []//]]. -by split=> //; apply: filterT. -Qed. -Lemma filter_prod2 {T U} {F : set (set T)} {G : set (set U)} - {FF : Filter F} (P : set U) : - (\forall y \near G, P y) -> \forall _ \near F & y \near G, P y. -Proof. -move=> FP; exists (setT, P)=> //= [|[?? []//]]. -by split=> //; apply: filterT. -Qed. - -Program Definition in_filter_prod {T U} {F : set (set T)} {G : set (set U)} - (P : in_filter F) (Q : in_filter G) : in_filter (filter_prod F G) := - @InFilter _ _ (fun x => prop_of P x.1 /\ prop_of Q x.2) _. +Program Definition filter_elt_prod {T U} {F : {filter T}} {G : {filter U}} + (P : filter_elt F) (Q : filter_elt G) : filter_elt (nbhs (F, G)) := + @FilterElt _ _ (fun x => prop_of P x.1 /\ prop_of Q x.2) _. Next Obligation. by exists (prop_of P, prop_of Q) => //=; split; apply: prop_ofP. Qed. -Lemma near_pair {T U} {F : set (set T)} {G : set (set U)} - {FF : Filter F} {FG : Filter G} - (P : in_filter F) (Q : in_filter G) x : - prop_of P x.1 -> prop_of Q x.2 -> prop_of (in_filter_prod P Q) x. +Lemma near_pair {T U} {F : {filter T}} {G : {filter U}} + {FF : is_filter F} {FG : is_filter G} + (P : filter_elt F) (Q : filter_elt G) x : + prop_of P x.1 -> prop_of Q x.2 -> prop_of (filter_elt_prod P Q) x. Proof. by case: x=> x y; do ?rewrite prop_ofE /=; split. Qed. -Lemma flim_fst {T U F G} {FG : Filter G} : - (@fst T U) @ filter_prod F G --> F. -Proof. by move=> P; apply: filter_prod1. Qed. - -Lemma flim_snd {T U F G} {FF : Filter F} : - (@snd T U) @ filter_prod F G --> G. -Proof. by move=> P; apply: filter_prod2. Qed. - -Lemma near_map {T U} (f : T -> U) (F : set (set T)) (P : set U) : - (\forall y \near f @ F, P y) = (\forall x \near F, P (f x)). -Proof. by []. Qed. - -Lemma near_map2 {T T' U U'} (f : T -> U) (g : T' -> U') - (F : set (set T)) (G : set (set T')) (P : U -> set U') : - Filter F -> Filter G -> - (\forall y \near f @ F & y' \near g @ G, P y y') = - (\forall x \near F & x' \near G , P (f x) (g x')). -Proof. -move=> FF FG; rewrite propeqE; split=> -[[A B] /= [fFA fGB] ABP]. - exists (f @^-1` A, g @^-1` B) => //= -[x y /=] xyAB. - by apply: (ABP (_, _)); apply: xyAB. -exists (f @` A, g @` B) => //=; last first. - by move=> -_ [/= [x Ax <-] [x' Bx' <-]]; apply: (ABP (_, _)). -rewrite !locally_simpl /filtermap /=; split. - by apply: filterS fFA=> x Ax; exists x. -by apply: filterS fGB => x Bx; exists x. -Qed. +Lemma cvg_fst {T U} (F : {filter T}) (G : {filter U}) : + (@fst T U) @ (F, G) --> nbhs F. +Proof. by move=> P; rewrite nearE; apply: filter_prod1. Qed. -Lemma near_mapi {T U} (f : T -> set U) (F : set (set T)) (P : set U) : - (\forall y \near f `@ F, P y) = (\forall x \near F, exists y, f x y /\ P y). -Proof. by []. Qed. +Lemma cvg_snd {T U} (F : {filter T}) (G : {filter U}) : + nbhs ((@snd T U) @ (F, G)) --> nbhs G. +Proof. by move=> P; rewrite nearE; apply: filter_prod2. Qed. -(* Lemma filterSpair (T T' : Type) (F : set (set T)) (F' : set (set T')) : *) -(* Filter F -> Filter F' -> *) +(* Lemma nearSpair (T T' : Type) (F : {filter T}) (F' : set (set T')) : *) +(* is_filter F -> is_filter F' -> *) (* forall (P : set T) (P' : set T') (Q : set (T * T')), *) (* (forall x x', P x -> P' x' -> Q (x, x')) -> F P /\ F' P' -> *) (* filter_prod F F' Q. *) (* Proof. *) (* move=> FF FF' P P' Q PQ [FP FP']; near=> x. *) (* have := PQ x.1 x.2; rewrite -surjective_pairing; apply; near: x; *) -(* by [apply: flim_fst|apply: flim_snd]. *) +(* by [apply: cvg_fst|apply: cvg_snd]. *) (* Grab Existential Variables. all: end_near. Qed. *) -Lemma filter_pair_near_of (T T' : Type) (F : set (set T)) (F' : set (set T')) : - Filter F -> Filter F' -> - forall (P : @in_filter T F) (P' : @in_filter T' F') (Q : set (T * T')), +Lemma filter_pair_near_of (T T' : Type) (F : {filter T}) (F' : {filter T'}) : + forall (P : @filter_elt T F) (P' : @filter_elt T' F') (Q : set (T * T')), (forall x x', prop_of P x -> prop_of P' x' -> Q (x, x')) -> - filter_prod F F' Q. + (nbhs (F, F')) Q. Proof. -move=> FF FF' [P FP] [P' FP'] Q PQ; rewrite prop_ofE in FP FP' PQ. -near=> x; have := PQ x.1 x.2; rewrite -surjective_pairing; apply; near: x; -by [apply: flim_fst|apply: flim_snd]. +move=> [P FP] [P' FP'] Q PQ; rewrite prop_ofE in FP FP' PQ. +by near=> x; have := PQ x.1 x.2; rewrite -surjective_pairing; apply; near: x; + by [apply: cvg_fst|apply: cvg_snd]. Grab Existential Variables. all: end_near. Qed. Tactic Notation "near=>" ident(x) ident(y) := (apply: filter_pair_near_of => x y ? ?). Tactic Notation "near" constr(F) "=>" ident(x) ident(y) := - apply: (have_near F); near=> x y. + apply: (near_const F); near=> x y. Module Export NearMap. -Definition near_simpl := (@near_simpl, @near_map, @near_mapi, @near_map2). -Ltac near_simpl := rewrite ?near_simpl. +Definition nearE := (@near_map, @near_mapi, @near_map2). +Ltac near_simpl := rewrite /= ?nearE /=. End NearMap. -Lemma flim_pair {T U V F} {G : set (set U)} {H : set (set V)} - {FF : Filter F} {FG : Filter G} {FH : Filter H} (f : T -> U) (g : T -> V) : - f @ F --> G -> g @ F --> H -> - (f x, g x) @[x --> F] --> (G, H). +Lemma nearN {T} {pfT : pfilterType T} (F : pfT) P : (* the converse impplication is for ultra filters *) + (\for x \near F, ~ P x) -> ~ \for x \near F, P x. Proof. -move=> fFG gFH P; rewrite !near_simpl => -[[A B] /=[GA HB] ABP]; near=> x. -by apply: (ABP (_, _)); split=> //=; near: x; [apply: fFG|apply: gFH]. +move=> FPN NFP; apply: (near_const F). +by apply: nearS2 FPN NFP => x Px/Px. +Qed. + +Section NearPair. +Context {T U V W : nonPropType}. +Context {fT : filterType T} {fU : filterType U} {fV : filterType V} {fW : filterType W}. + + + +Lemma cvg_pair {F : {filter T}} {G : {filter U}} {H : {filter V}} + (f : T -> U) (g : T -> V) : + f @ F --> G -> g @ F --> H -> (f x, g x) @[x --> F] --> (G, H). +Proof. +move=> fFG gFH /= P [[/=A B] [GA HB] ABP]; rewrite near_map; near=> x => /=. +by apply: ABP; split=> /=; near: x; [apply: fFG|apply: gFH]. Grab Existential Variables. all: end_near. Qed. -Lemma flim_comp2 {T U V W} - {F : set (set T)} {G : set (set U)} {H : set (set V)} {I : set (set W)} - {FF : Filter F} {FG : Filter G} {FH : Filter H} +(* Lemma cvg_pair {F : fT} {G : fU} {H : fV} (f : T -> U) (g : T -> V) : *) +(* f @ F --> G -> g @ F --> H -> (f x, g x) @[x --> F] --> (G, H). *) +(* Proof. *) +(* move=> fFG gFH /= P [[/=A B] [GA HB] ABP]; rewrite near_map; near=> x. *) +(* by apply: ABP; split=> /=; near: x; [apply: fFG|apply: gFH]. *) +(* Grab Existential Variables. all: end_near. Qed. *) + +(* Lemma cvg_comp2 {F : fT} {G : fU} {H : fV} {I : fW} *) +(* (f : T -> U) (g : T -> V) (h : U -> V -> W) : *) +(* f @ F --> G -> g @ F --> H -> *) +(* h (fst x) (snd x) @[x --> (G, H)] --> I -> *) +(* h (f x) (g x) @[x --> F] --> I. *) +(* Proof. *) +(* move=> fFG gFH hGHI P /= IP; rewrite nearE in hGHI *. *) +(* suff: \for w \near (f x, g x) @[x --> F], P (h w.1 w.2) by rewrite !nearE. *) +(* by apply: (cvg_pair fFG gFH); apply: hGHI. *) +(* Qed. *) +Lemma cvg_comp2 {F : {filter T}} {G : {filter U}} {H : {filter V}} {I : {filter W}} (f : T -> U) (g : T -> V) (h : U -> V -> W) : f @ F --> G -> g @ F --> H -> h (fst x) (snd x) @[x --> (G, H)] --> I -> h (f x) (g x) @[x --> F] --> I. -Proof. by move=> fFG gFH hGHI P /= IP; apply: flim_pair (hGHI _ IP). Qed. -Arguments flim_comp2 {T U V W F G H I FF FG FH f g h} _ _ _. -Definition flim_comp_2 := @flim_comp2. - -(* Lemma flimi_comp_2 {T U V W} *) -(* {F : set (set T)} {G : set (set U)} {H : set (set V)} {I : set (set W)} *) -(* {FF : Filter F} *) -(* (f : T -> U) (g : T -> V) (h : U -> V -> set W) : *) -(* f @ F --> G -> g @ F --> H -> *) -(* h (fst x) (snd x) `@[x --> (G, H)] --> I -> *) -(* h (f x) (g x) `@[x --> F] --> I. *) -(* Proof. *) -(* intros Cf Cg Ch. *) -(* change (fun x => h (f x) (g x)) with (fun x => h (fst (f x, g x)) (snd (f x, g x))). *) -(* apply: flimi_comp Ch. *) -(* now apply flim_pair. *) -(* Qed. *) +Proof. +move=> fFG gFH hGHI P /= IP; rewrite nearE in hGHI *. +suff: \for w \near (f x, g x) @[x --> F], P (h w.1 w.2) by rewrite !nearE. +by apply: (cvg_pair fFG gFH); apply: hGHI. +Qed. + +End NearPair. +(* Arguments cvg_comp2 {T U V W fT fU fV fW F G H I f g h} _ _ _. *) +Arguments cvg_comp2 {T U V W F G H I f g h} _ _ _. (** Restriction of a filter to a domain *) -Definition within {T : Type} (D : set T) (F : set (set T)) (P : set T) := - {near F, D `<=` P}. +Section Within. +Context {T : Type} {fT : filterType T}. +Implicit Types (A D P : set T) (F : fT). + +Definition within D F := [set P : set T | {near F, D `<=` P}]. Arguments within : simpl never. -Lemma near_withinE {T : Type} (D : set T) (F : set (set T)) (P : set T) : - (\forall x \near within D F, P x) = {near F, D `<=` P}. +Lemma near_withinE D F P : + (\for x \near within D F, P x) = {near F, D `<=` P}. Proof. by []. Qed. -Lemma withinT {T : Type} (F : set (set T)) (A : set T) : Filter F -> within A F A. -Proof. by move=> FF; rewrite /within; apply: filterE. Qed. - -Lemma near_withinT {T : Type} (F : set (set T)) (A : set T) : Filter F -> - (\forall x \near within A F, A x). -Proof. exact: withinT. Qed. +Lemma withinT D F : nbhs (within D F) D. +Proof. by rewrite /within; apply: near_all. Qed. -Global Instance within_filter T D F : Filter F -> Filter (@within T D F). +Lemma within_filter D F : is_filter (within D F). Proof. -move=> FF; rewrite /within; constructor. -- by apply: filterE. -- by move=> P Q; apply: filterS2 => x DP DQ Dx; split; [apply: DP|apply: DQ]. -- by move=> P Q subPQ; apply: filterS => x DP /DP /subPQ. +rewrite /within; constructor. +- by apply: near_all. +- by move=> P Q; apply: nearS2 => x DP DQ Dx; split; [apply: DP|apply: DQ]. +- by move=> P Q subPQ; apply: nearS => x DP /DP /subPQ. Qed. -Typeclasses Opaque within. -Canonical within_filter_on T D (F : filter_on T) := - FilterType (within D F) (within_filter _ _). +Canonical within_filterType D F := Eval hnf in + Filter (within D F) (within_filter _ _). -Lemma flim_within {T} {F : set (set T)} {FF : Filter F} D : - within D F --> F. -Proof. by move=> P; apply: filterS. Qed. +Lemma cvg_within D F : within D F --> F. +Proof. by move=> P; apply: nearS. Qed. -Definition subset_filter {T} (F : set (set T)) (D : set T) := - [set P : set {x | D x} | F [set x | forall Dx : D x, P (exist _ x Dx)]]. -Arguments subset_filter {T} F D _. +Definition subset_sig D F := + [set P : set {x | D x} | \for x \near F, forall Dx : D x, P (exist _ x Dx)]. +Arguments subset_sig D F _ : clear implicits. -Global Instance subset_filter_filter T F (D : set T) : - Filter F -> Filter (subset_filter F D). +Lemma subset_sig_is_filter D F : is_filter (Nbhs (subset_sig D F)). Proof. -move=> FF; constructor; rewrite /subset_filter. -- exact: filterE. -- by move=> P Q; apply: filterS2=> x PD QD Dx; split. -- by move=> P Q subPQ; apply: filterS => R PD Dx; apply: subPQ. +constructor; rewrite /subset_sig. +- exact: near_all. +- by move=> P Q; apply: nearS2=> x PD QD Dx; split. +- by move=> P Q subPQ; apply: nearS => R PD Dx; apply: subPQ. Qed. -Typeclasses Opaque subset_filter. +Canonical subset_sig_filterType D F := Eval hnf in + Filter (subset_sig D F) (subset_sig_is_filter _ _). -Lemma subset_filter_proper {T F} {FF : Filter F} (D : set T) : - (forall P, F P -> ~ ~ exists x, D x /\ P x) -> - ProperFilter (subset_filter F D). +Lemma subset_sig_proper D F : + (forall P, nbhs F P -> ~ ~ exists x, D x /\ P x) -> + is_pfilter (subset_sig D F). Proof. -move=> DAP; apply: Build_ProperFilter'; rewrite /subset_filter => subFD. +move=> DAP; apply: Build_is_pfilter'; first exact: filter_class. +rewrite /subset_sig => subFD. by have /(_ subFD) := DAP (~` D); apply => -[x [dx /(_ dx)]]. Qed. +End Within. + (** * Topological spaces *) Module Topological. -Record mixin_of (T : Type) (locally : T -> set (set T)) := Mixin { - open : set (set T) ; - ax1 : forall p : T, ProperFilter (locally p) ; - ax2 : forall p : T, locally p = - [set A : set T | exists B : set T, open B /\ B p /\ B `<=` A] ; - ax3 : open = [set A : set T | A `<=` locally^~ A ] +Record mixin_of (T : Type) (nbhs : T -> set (set T)) := Mixin { + open : set (set T); + ax2 : forall p : T, nbhs p = + [set A : set T | exists B : set T, [/\ open B, B p & B `<=` A]] ; + ax3 : open = [set A : set T | A `<=` nbhs^~ A ] }. Record class_of (T : Type) := Class { - base : Filtered.class_of T T; - mixin : mixin_of (Filtered.locally_op base) + base : PFilter.class_of T T; + mixin : mixin_of (Nbhs.nbhs_op base) }. Section ClassDef. @@ -1258,25 +1334,27 @@ Definition class := let: Pack _ c _ := cT return class_of cT in c. Definition clone c of phant_id class c := @Pack T c T. Let xT := let: Pack T _ _ := cT in T. Notation xclass := (class : class_of xT). -Local Coercion base : class_of >-> Filtered.class_of. +Local Coercion base : class_of >-> PFilter.class_of. Local Coercion mixin : class_of >-> mixin_of. Definition pack loc (m : @mixin_of T loc) := - fun bT (b : Filtered.class_of T T) of phant_id (@Filtered.class T bT) b => - fun m' of phant_id m (m' : @mixin_of T (Filtered.locally_op b)) => + fun bT (b : PFilter.class_of T T) of phant_id (@PFilter.class T bT) b => + fun m' of phant_id m (m' : @mixin_of T (Nbhs.nbhs_op b)) => @Pack T (@Class _ b m') T. Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. -Definition pointedType := @Pointed.Pack cT xclass xT. -Definition filteredType := @Filtered.Pack cT cT xclass xT. +Definition pointedType := @Pointed.Pack cT xclass. +Definition nbhsType := @Nbhs.Pack cT cT xclass. +Definition filterType := @Filter.Pack cT cT xclass. +Definition pfilterType := @PFilter.Pack cT cT xclass. End ClassDef. Module Exports. Coercion sort : type >-> Sortclass. -Coercion base : class_of >-> Filtered.class_of. +Coercion base : class_of >-> PFilter.class_of. Coercion mixin : class_of >-> mixin_of. Coercion eqType : type >-> Equality.type. Canonical eqType. @@ -1284,8 +1362,12 @@ Coercion choiceType : type >-> Choice.type. Canonical choiceType. Coercion pointedType : type >-> Pointed.type. Canonical pointedType. -Coercion filteredType : type >-> Filtered.type. -Canonical filteredType. +Coercion nbhsType : type >-> Nbhs.type. +Canonical nbhsType. +Coercion filterType : type >-> Filter.type. +Canonical filterType. +Coercion pfilterType : type >-> PFilter.type. +Canonical pfilterType. Notation topologicalType := type. Notation TopologicalType T m := (@pack T _ m _ _ idfun _ idfun). Notation TopologicalMixin := Mixin. @@ -1308,83 +1390,82 @@ Definition open := Topological.open (Topological.class T). Definition neigh (p : T) (A : set T) := open A /\ A p. -Global Instance locally_filter (p : T) : ProperFilter (locally p). -Proof. by apply: Topological.ax1; case: T p => ? []. Qed. -Typeclasses Opaque locally. - -Canonical locally_filter_on (x : T) := - FilterType (locally x) (@filter_filter' _ _ (locally_filter x)). - -Lemma locallyE (p : T) : - locally p = [set A : set T | exists B : set T, neigh p B /\ B `<=` A]. +Lemma open_nbhsE (p : T) : + (nbhs p) = + [set A : set T | exists B : set T, neigh p B /\ B `<=` A] :> set _. Proof. -have -> : locally p = [set A : set T | exists B, open B /\ B p /\ B `<=` A]. +have -> : (nbhs p) = [set A : set T | exists B, [/\ open B, B p & B `<=` A]] :> set _. exact: Topological.ax2. -by rewrite predeqE => A; split=> [[B [? []]]|[B [[]]]]; exists B. +by rewrite predeqE => A; split=> [[B [?]]|[B [[]]]]; exists B. Qed. -Definition interior (A : set T) := (@locally _ [filteredType T of T])^~ A. +Definition interior (A : set T) : set T := [set x | (nbhs x) A]. Local Notation "A ^°" := (interior A). Lemma interior_subset (A : set T) : A^° `<=` A. Proof. -by move=> p; rewrite /interior locallyE => -[? [[??]]]; apply. +by move=> p; rewrite /interior open_nbhsE => -[? [[? ?]]]; apply. Qed. Lemma openE : open = [set A : set T | A `<=` A^°]. Proof. exact: Topological.ax3. Qed. -Lemma locally_singleton (p : T) (A : set T) : locally p A -> A p. -Proof. by rewrite locallyE => - [? [[_ ?]]]; apply. Qed. +Lemma nbhs_singleton (p : T) (A : set T) : (nbhs p) A -> A p. +Proof. by rewrite open_nbhsE => - [? [[_ ?]]]; apply. Qed. -Lemma locally_interior (p : T) (A : set T) : locally p A -> locally p A^°. +Lemma nbhs_interior (p : T) (A : set T) : (nbhs p) A -> (nbhs p) A^°. Proof. -rewrite locallyE /neigh openE => - [B [[Bop Bp] sBA]]. -by exists B; split=> // q Bq; apply: filterS sBA _; apply: Bop. -Qed. +rewrite open_nbhsE /neigh openE => - [B [[Bop Bp] sBA]]. +exists B; split=> // q Bq; rewrite /interior. +by near=> x; apply: sBA; near: x; apply: Bop. +Grab Existential Variables. all: end_near. Qed. + +Lemma nbhs_expand (p : T) (A : set T) : + (\for x \near p, A x) -> (\for x \near p, \for y \near x, A y). +Proof. exact: nbhs_interior. Qed. Lemma open0 : open set0. Proof. by rewrite openE. Qed. Lemma openT : open setT. -Proof. by rewrite openE => ??; apply: filterT. Qed. +Proof. by rewrite openE => ? ?; apply: nearT. Qed. Lemma openI (A B : set T) : open A -> open B -> open (A `&` B). Proof. rewrite openE => Aop Bop p [Ap Bp]. -by apply: filterI; [apply: Aop|apply: Bop]. +by apply: nearI; [apply: Aop|apply: Bop]. Qed. Lemma open_bigU (I : Type) (D : set I) (f : I -> set T) : (forall i, D i -> open (f i)) -> open (\bigcup_(i in D) f i). Proof. rewrite openE => fop p [i Di]. -by have /fop fiop := Di; move/fiop; apply: filterS => ??; exists i. +by have /fop fiop := Di; move/fiop; apply: nearS => ? ?; exists i. Qed. Lemma openU (A B : set T) : open A -> open B -> open (A `|` B). Proof. -by rewrite openE => Aop Bop p [/Aop|/Bop]; apply: filterS => ??; [left|right]. +by rewrite openE => Aop Bop p [/Aop|/Bop]; apply: nearS => ? ?; [left|right]. Qed. Lemma open_subsetE (A B : set T) : open A -> (A `<=` B) = (A `<=` B^°). Proof. rewrite openE => Aop; rewrite propeqE; split. - by move=> sAB p Ap; apply: filterS sAB _; apply: Aop. + by move=> sAB p Ap; apply: nearS sAB _; apply: Aop. by move=> sAB p /sAB /interior_subset. Qed. Lemma open_interior (A : set T) : open A^°. Proof. -rewrite openE => p; rewrite /interior locallyE => - [B [[Bop Bp]]]. +rewrite openE => p; rewrite /interior open_nbhsE => - [B [[Bop Bp]]]. by rewrite open_subsetE //; exists B. Qed. Lemma interior_bigcup I (D : set I) (f : I -> set T) : \bigcup_(i in D) (f i)^° `<=` (\bigcup_(i in D) f i)^°. Proof. -move=> p [i Di]; rewrite /interior locallyE => - [B [[Bop Bp] sBfi]]. +move=> p [i Di]; rewrite /interior open_nbhsE => - [B [[Bop Bp] sBfi]]. by exists B; split=> // ? /sBfi; exists i. Qed. @@ -1395,8 +1476,8 @@ Lemma neighI (p : T) (A B : set T) : neigh p A -> neigh p B -> neigh p (A `&` B). Proof. by move=> [Aop Ap] [Bop Bp]; split; [apply: openI|split]. Qed. -Lemma neigh_locally (p : T) (A : set T) : neigh p A -> locally p A. -Proof. by rewrite locallyE => p_A; exists A; split. Qed. +Lemma neigh_nbhs (p : T) (A : set T) : neigh p A -> (nbhs p) A. +Proof. by rewrite open_nbhsE => p_A; exists A; split. Qed. End Topological1. @@ -1407,22 +1488,23 @@ Notation continuous f := (forall x, f%function @ x --> f%function x). Lemma continuous_cst (S T : topologicalType) (a : T) : continuous (fun _ : S => a). Proof. -move=> x A; rewrite !locally_simpl /= !locallyE => - [B [[_ Ba] sBA]]. -by exists setT; split; [apply: neighT|move=> ??; apply: sBA]. -Qed. +move=> x A; rewrite open_nbhsE => - [B [[_ Ba] sBA]]. +by rewrite nearE; near=> y; apply: sBA. +Grab Existential Variables. all: end_near. Qed. Lemma continuousP (S T : topologicalType) (f : S -> T) : continuous f <-> forall A, open A -> open (f @^-1` A). Proof. -split=> fcont; first by rewrite !openE => A Aop ? /Aop /fcont. -move=> s A; rewrite locally_simpl /= !locallyE => - [B [[Bop Bfs] sBA]]. -by exists (f @^-1` B); split; [split=> //; apply/fcont|move=> ? /sBA]. -Qed. +split=> fcont; first by rewrite !openE => A Aop ? /Aop /fcont; rewrite nearE. +move=> s A; rewrite open_nbhsE => - [B [[Bop Bfs] sBA]]. +rewrite nearE; near=> y; apply: sBA; near: y. +by apply: neigh_nbhs; rewrite /neigh; split => //; apply: fcont. +Grab Existential Variables. all: end_near. Qed. Lemma continuous_comp (R S T : topologicalType) (f : R -> S) (g : S -> T) x : {for x, continuous f} -> {for (f x), continuous g} -> {for x, continuous (g \o f)}. -Proof. exact: flim_comp. Qed. +Proof. exact: cvg_comp. Qed. Lemma open_comp {T U : topologicalType} (f : T -> U) (D : set U) : {in f @^-1` D, continuous f} -> open D -> open (f @^-1` D). @@ -1432,13 +1514,13 @@ by apply: fcont; [rewrite in_setE|apply: Dop]. Qed. Lemma is_filter_lim_filtermap {T: topologicalType} {U : topologicalType} - (F : set (set T)) x (f : T -> U) : + (F : {filter T}) x (f : T -> U) : {for x, continuous f} -> F --> x -> f @ F --> f x. Proof. by move=> cf fx P /cf /fx. Qed. Lemma near_join (T : topologicalType) (x : T) (P : set T) : (\near x, P x) -> \near x, \near x, P x. -Proof. exact: locally_interior. Qed. +Proof. exact: nbhs_interior. Qed. Lemma near_bind (T : topologicalType) (P Q : set T) (x : T) : (\near x, (\near x, P x) -> Q x) -> (\near x, P x) -> \near x, Q x. @@ -1449,145 +1531,333 @@ Grab Existential Variables. all: end_near. Qed. (* limit composition *) -Lemma lim_cont {T : Type} {V U : topologicalType} - (F : set (set T)) (FF : Filter F) +Lemma lim_cont {T : Type} {V U : topologicalType} {fT : filterType T} (F : fT) (f : T -> V) (h : V -> U) (a : V) : {for a, continuous h} -> f @ F --> a -> (h \o f) @ F --> h a. Proof. -move=> h_cont fa fb; apply: (flim_trans _ h_cont). -exact: (@flim_comp _ _ _ _ h _ _ _ fa). +by move=> h_cont fa fb; apply: (cvg_trans _ h_cont); apply: @cvg_comp fa _. Qed. -Lemma lim_cont2 {T : Type} {V W U : topologicalType} - (F : set (set T)) (FF : Filter F) - (f : T -> V) (g : T -> W) (h : V -> W -> U) (a : V) (b : W) : - h z.1 z.2 @[z --> (a, b)] --> h a b -> - f @ F --> a -> g @ F --> b -> (fun x => h (f x) (g x)) @ F --> h a b. -Proof. -move=> h_cont fa fb; apply: (flim_trans _ h_cont). -exact: (@flim_comp _ _ _ _ (fun x => h x.1 x.2) _ _ _ (flim_pair fa fb)). -Qed. - -Lemma cst_continuous {T : Type} {T' : topologicalType} (k : T') - (F : set (set T)) {FF : Filter F} : +Lemma cst_continuous {T : Type} {T' : topologicalType} (k : T') (F : {filter T}) : (fun _ : T => k) @ F --> k. -Proof. -by move=> x; rewrite !near_simpl => /locally_singleton ?; apply: filterE. -Qed. -Arguments cst_continuous {T T'} k F {FF}. +Proof. by move=> x /nbhs_singleton ?; apply: near_all. Qed. +Arguments cst_continuous {T T'} k F. Hint Resolve cst_continuous : core. (** ** Topology defined by a filter *) Section TopologyOfFilter. -Context {T : Type} {loc : T -> set (set T)}. -Hypothesis (loc_filter : forall p : T, ProperFilter (loc p)). +Context {T : pointedType} {loc : T -> {filter T}}. Hypothesis (loc_singleton : forall (p : T) (A : set T), loc p A -> A p). Hypothesis (loc_loc : forall (p : T) (A : set T), loc p A -> loc p (loc^~ A)). -Definition open_of_locally := [set A : set T | A `<=` loc^~ A]. +Definition open_of_nbhs := [set A : set T | A `<=` loc^~ A]. Program Definition topologyOfFilterMixin : Topological.mixin_of loc := - @Topological.Mixin T loc open_of_locally _ _ _. + @Topological.Mixin T loc open_of_nbhs _ _. Next Obligation. rewrite predeqE => A; split=> [p_A|]; last first. - by move=> [B [Bop [Bp sBA]]]; apply: filterS sBA _; apply: Bop. -exists (loc^~ A); split; first by move=> ?; apply: loc_loc. -by split => // q /loc_singleton. + move=> [B [Bop Bp sBA]]. + rewrite -filter_setE/=. + by apply: nearS sBA _; apply: Bop. +exists (loc^~ A); split => //; do ?by move=> ?; apply: loc_loc. +by move=> // q /loc_singleton. Qed. End TopologyOfFilter. +Section Prod_Topology. + +Context {T U : topologicalType}. + +Lemma prod_loc_singleton (p : T * U) (A : set (T * U)) : nbhs p A -> A p. +Proof. +by move=> [QR [/nbhs_singleton Qp1 /nbhs_singleton Rp2]]; apply. +Qed. + +Lemma prod_loc_loc (p : T * U) (A : set (T * U)) : + nbhs p A -> nbhs p (nbhs^~ A). +Proof. +move=> [QR [/nbhs_interior p1_Q /nbhs_interior p2_R] sQRA]. +by exists (QR.1^°, QR.2^°) => // ? ?; exists QR. +Qed. + +Definition prod_topologicalTypeMixin := + topologyOfFilterMixin prod_loc_singleton prod_loc_loc. + +Canonical prod_topologicalType := Eval hnf in + TopologicalType (T * U) prod_topologicalTypeMixin. + +End Prod_Topology. + +Definition filter_of T (x : set (set T)) := + fun (F : filter_on T) of phant_id x (in_filter F) => F. +Notation "[ 'filter' 'of' x ]" := (@filter_of _ x _ idfun). + +Lemma lim_cont2 {T : Type} {V W U : topologicalType} {fT : filterType T} (F : fT) + (f : T -> V) (g : T -> W) (h : V -> W -> U) (a : V) (b : W) : + h z.1 z.2 @[z --> (a, b)] --> h a b -> + f @ F --> a -> g @ F --> b -> (h (f x) (g x))@[x --> F] --> h a b. +Proof. +(* suff: False by []. *) +(* move: (fun z : V * W => h z.1 z.2) => uh. *) +(* move: (a, b) => ab. *) +(* evar (fU : filterType U). *) +(* evar (x : Filter.sort fU). *) +(* Print Canonical Projections. *) +(* unify (in_nbhs ?x) (uh @ ab). *) + +move=> hc fa fb; apply: cvg_trans hc. +by apply: (cvg_comp2 fa fb). + +(* appl *) +(* apply. *) +(* move=> /(_ _ _ _ h)/=. *) +(* move: ((fun x : T => h (f x) (g x)) @ F) => G. *) +(* move: (fun z : V * W => h z.1 z.2) => uh. *) +(* move: (a, b) => ab. *) +(* rewrite {T fT F f g h a b fa fb}. *) +(* (* pose x := [filter of uh @ ab]. *) *) +(* (* rewrite -[uh @ ab]/(in_filter x). *) *) +(* move=> /(_ [filterType U of filter_on U])/=. *) + +(* (* rewrite /cvg_to/=. *) *) +(* (* rewrite -[in_nbhs (nbhs (uh @ ab))]/(uh @ ab). *) *) +(* (* evar (fU : filterType U). *) *) +(* (* move=> /(_ ?fU). *) *) +(* (* evar (s : Filter.sort [filterType U of filter_on U]). *) *) +(* move: (@cvg_to) => cvgto /=. *) +(* set daf := default_arrow_filter _. *) + +(* unify (in_bhs (nbhs (uh @ ab)) (nbhs ?s). *) +(* apply. *) + + +(* apply. *) +(* rewrite nbhs_setE. *) + + +(* move: (@cvg_to) => cvgto /=. *) +(* set daf := default_arrow_filter _. *) +(* apply. *) +(* move: cvg_to. *) +(* move: cvg_to. *) +(* set u := subset. *) + +(* move=> /(_ _ x). *) +(* pose X := [filterType U of (filter_on U)]. *) +(* move=> /(_ X). *) +(* apply. *) + +(* set x := uh @ ab. *) + + + +(* rewrite /nbhs. *) +(* have := *) + + +(* (* evar (fU : filterType U). *) *) +(* Set Printing All. *) +(* apply. *) + + +(* pose nbhsU := [filterType U of filter_on U]. *) +(* move=> /(_ nbhsU). *) + +(* Set Printing Coercions. *) +(* apply. *) +(* have : (Filter.sort U) = (filter_on U). *) +(* reflexivity. *) +(* unify (Filter.sort U) (filter_on U). *) +(* pose nbhsU := [filterType U of filter_on U]. *) +(* move=> /(_ nbhsU). *) +(* apply. *) +(* apply. *) +(* (* nbhs ?s *) *) +(* (* uh @ ab *) *) +(* move=> /(_ _ _ (@cvg_refl _ (nbhs (uh @ ab)))). *) +(* move=> XX. *) +(* Set Printing All. *) +(* apply XX. *) +(* apply. *) + + +(* rewrite /cvg. *) +(* apply. *) +(* apply. *) + +(* apply. *) +(* apply: cvg_comp2 fa fb _. Qed. *) +Qed. + (** ** Topology defined by open sets *) -Section TopologyOfOpen. +Module OfOpen. +Section OfOpen. -Variable (T : Type) (op : set T -> Prop). +Variable (T : pointedType). +Definition type : Type := T. +Variable (op : set type -> Prop). Hypothesis (opT : op setT). -Hypothesis (opI : forall (A B : set T), op A -> op B -> op (A `&` B)). -Hypothesis (op_bigU : forall (I : Type) (f : I -> set T), +Hypothesis (opI : forall (A B : set type), op A -> op B -> op (A `&` B)). +Hypothesis (op_bigU : forall (I : Type) (f : I -> set type), (forall i, op (f i)) -> op (\bigcup_i f i)). -Definition locally_of_open (p : T) (A : set T) := - exists B, op B /\ B p /\ B `<=` A. +Canonical pointedType := Eval hnf in [pointedType of type]. -Program Definition topologyOfOpenMixin : Topological.mixin_of locally_of_open := - @Topological.Mixin T locally_of_open op _ _ _. -Next Obligation. -apply Build_ProperFilter. - by move=> A [B [_ [Bp sBA]]]; exists p; apply: sBA. -split; first by exists setT. - move=> A B [C [Cop [Cp sCA]]] [D [Dop [Dp sDB]]]. - exists (C `&` D); split; first exact: opI. - by split=> // q [/sCA Aq /sDB Bq]. -move=> A B sAB [C [Cop [p_C sCA]]]. -by exists C; split=> //; split=> //; apply: subset_trans sAB. +Definition nbhsMixin : Nbhs.mixin_of type type := + NbhsMixin_ (fun p => [set A | exists B, [/\ op B, B p & B `<=` A]]). +Canonical nbhsType := Eval hnf in NbhsType type type nbhsMixin. + +Lemma filterMixin : Filter.mixin_of [nbhsType type of type]. +Proof. +constructor=> x; split; first by exists setT. + move=> A B [OA [OPop OAp OAA] [OB [OBop OBp OBB]]]. + by exists (OA `&` OB); split => //; [exact: opI|exact: subsetI2]. +by move=> A B AB [OA [OPop OAp OAA]]; exists OA; split => // y /OAA /AB. Qed. -Next Obligation. +Canonical filterType := Eval hnf in FilterType type type filterMixin. + +Lemma pfilterMixin : PFilter.mixin_of [filterType type of type]. +Proof. by constructor => x; move=> [O [Oop Op]] /(_ _ Op). Qed. +Canonical pfilterType := Eval hnf in PFilterType type type pfilterMixin. + +Fact nbhs_of_openE : op = [set A : set type | A `<=` nbhs^~ A]. +Proof. rewrite predeqE => A; split=> [Aop p Ap|Aop]. by exists A; split=> //; split. -suff -> : A = \bigcup_(B : {B : set T & op B /\ B `<=` A}) projT1 B. +suff -> : A = \bigcup_(B : {B : set type & op B /\ B `<=` A}) projT1 B. by apply: op_bigU => B; have [] := projT2 B. rewrite predeqE => p; split=> [|[B _ Bp]]; last by have [_] := projT2 B; apply. -by move=> /Aop [B [Bop [Bp sBA]]]; exists (existT _ B (conj Bop sBA)). +by move=> /Aop [B [Bop Bp sBA]]; exists (existT _ B (conj Bop sBA)). +Qed. + +Definition topologyMixin : Topological.mixin_of (nbhs : type -> set (set type)) := + Topological.Mixin (fun=> erefl) nbhs_of_openE. +Canonical topologicalType := Eval hnf in TopologicalType type topologyMixin. + +End OfOpen. +End OfOpen. + + +Lemma bigcup1 (I R : Type) (i : I) (F : I -> set R) : + \bigcup_(j in [set i]) F j = F i. +Proof. by rewrite predeqE => x; split=> [[j->//]|]; exists i. Qed. + +Lemma in_nbhs_inj T : injective (@in_nbhs T). +Proof. by move=> [A] [B]; rewrite /in_nbhs => ->. Qed. + +Notation flip f := (fun x y => f y x). +Definition imagei U V (f : U -> V -> Prop) (A : set U) : set V := + [set v | exists2 u, A u & f u v]. +Definition preimagei U V (f : U -> V -> Prop) (B : set V) : set U := + imagei (flip f) B. + +Lemma bigcup_image I J (f : I -> J -> Prop) R (F : J -> set R) (A : set I) : + \bigcup_(j in imagei f A) F j = \bigcup_(i in A) \bigcup_(j in f i) F j. +Proof. +rewrite predeqE => x; split=> [[j [i Ai fij] Fjx]|[i Ai [j fij Fjx]]]. + by exists i => //; exists j. +by exists j => //; exists i. +Qed. + +Lemma predeqP T (A B : set T) : (A = B) <-> (A `<=>` B). +Proof. +by rewrite predeqE; split=> [AB|[AB BA]]; split=> ? *; by [apply/AB|apply/BA]. Qed. -End TopologyOfOpen. +Lemma eq_bigcup I R (F G : I -> set R) (A B : set I) : + A `<=>` B -> (forall x, A x -> F x = G x) -> + \bigcup_(i in A) F i = \bigcup_(i in B) G i. +Proof. +move=> /predeqP <- eqFG; rewrite predeqE=> x. +by split=> -[i Bi Pix]; exists i => //; rewrite ?eqFG// -?eqFG. +Qed. + +Lemma eq_bigcupr I R (F G : I -> set R) (A : set I) : + (forall x, A x -> F x = G x) -> + \bigcup_(i in A) F i = \bigcup_(i in A) G i. +Proof. by move=> /eq_bigcup; apply; split. Qed. (** ** Topology defined by a base of open sets *) -Section TopologyOfBase. +Module OfBase. +Section OfBase. + +Variable (I : Type) (T : pointedType) (D : set I) (b : I -> set T). +Definition type : Type := T. -Definition open_from I T (D : set I) (b : I -> set T) := - [set \bigcup_(i in D') b i | D' in subset^~ D]. +Definition open_of : set (set type) := + [set A | exists E, E `<=` D /\ A = \bigcup_(i in E) b i]. -Lemma open_fromT I T (D : set I) (b : I -> set T) : - \bigcup_(i in D) b i = setT -> open_from D b setT. -Proof. by move=> ?; exists D. Qed. +Definition nbhs_of (p : type) : set (set type) := + [set A | exists i, [/\ D i, b i p & b i `<=` A]]. + +Canonical pointedType := Eval hnf in [pointedType of type]. + +Definition nbhsMixin : Nbhs.mixin_of type type := NbhsMixin_ nbhs_of. +Canonical nbhsType := Eval hnf in NbhsType type type nbhsMixin. -Variable (I : pointedType) (T : Type) (D : set I) (b : I -> (set T)). Hypothesis (b_cover : \bigcup_(i in D) b i = setT). Hypothesis (b_join : forall i j t, D i -> D j -> b i t -> b j t -> - exists k, D k /\ b k t /\ b k `<=` b i `&` b j). + exists k, [/\ D k, b k t & b k `<=` b i `&` b j]). -Program Definition topologyOfBaseMixin := - @topologyOfOpenMixin _ (open_from D b) (open_fromT b_cover) _ _. -Next Obligation. -have [DA sDAD AeUbA] := H; have [DB sDBD BeUbB] := H0. -have ABU : forall t, (A `&` B) t -> - exists it, D it /\ b it t /\ b it `<=` A `&` B. - move=> t [At Bt]. - have [iA [DiA [biAt sbiA]]] : exists i, D i /\ b i t /\ b i `<=` A. - move: At; rewrite -AeUbA => - [i DAi bit]; exists i. - by split; [apply: sDAD|split=> // ?; exists i]. - have [iB [DiB [biBt sbiB]]] : exists i, D i /\ b i t /\ b i `<=` B. - move: Bt; rewrite -BeUbB => - [i DBi bit]; exists i. - by split; [apply: sDBD|split=> // ?; exists i]. - have [i [Di [bit sbiAB]]] := b_join DiA DiB biAt biBt. - by exists i; split=> //; split=> // s /sbiAB [/sbiA ? /sbiB]. -set Dt := fun t => [set it | D it /\ b it t /\ b it `<=` A `&` B]. -exists [set get (Dt t) | t in A `&` B]. - by move=> _ [t ABt <-]; have /ABU/getPex [] := ABt. -rewrite predeqE => t; split=> [[_ [s ABs <-] bDtst]|ABt]. - by have /ABU/getPex [_ [_]] := ABs; apply. -by exists (get (Dt t)); [exists t| have /ABU/getPex [? []]:= ABt]. +Fact geti (x : type) : exists2 i, D i & b i x. +Proof. +have: True by []; have /(congr1 (@^~ x))/= := b_cover; rewrite /setT => <-. +by move=> [i Di]; exists i. Qed. -Next Obligation. -set fop := fun j => [set Dj | Dj `<=` D /\ f j = \bigcup_(i in Dj) b i]. -exists (\bigcup_j get (fop j)). - move=> i [j _ fopji]. - suff /getPex [/(_ _ fopji)] : exists Dj, fop j Dj by []. - by have [Dj] := H j; exists Dj. -rewrite predeqE => t; split=> [[i [j _ fopji bit]]|[j _]]. - exists j => //; suff /getPex [_ ->] : exists Dj, fop j Dj by exists i. - by have [Dj] := H j; exists Dj. -have /getPex [_ ->] : exists Dj, fop j Dj by have [Dj] := H j; exists Dj. -by move=> [i]; exists i => //; exists j. + +Lemma filterMixin : Filter.mixin_of [nbhsType type of type]. +Proof. +constructor=> x; split. + by have [i Di bix] := geti x; exists i. +move=> A B [i [Di bix biA]] [j [Dj bjx bjB]]. + have [||||k [Dk bkx bkij]] // := @b_join i j x. + by exists k; split => //; apply: subset_trans bkij _; apply: subsetI2. +by move=> A B AB [i [Di bix biA]]; exists i; split => // y /biA /AB. Qed. +Canonical filterType := Eval hnf in FilterType type type filterMixin. -End TopologyOfBase. +Lemma pfilterMixin : PFilter.mixin_of [filterType type of type]. +Proof. by constructor => x; move=> [O [Oop Op]] /(_ _ Op). Qed. +Canonical pfilterType := Eval hnf in PFilterType type type pfilterMixin. + +Notation base_nbhs p := [set A | exists B, [/\ open_of B, B p & B `<=` A]]. + +Lemma nbhs_open (p : type) : nbhs p = base_nbhs p :> set _. +Proof. +rewrite predeqE => A; split => [[i [Di bip biA]]|[O [[E [ED ->]] Op OA]]]. + exists (b i); split => //; exists [set i]. + by split => [j ->//|]; rewrite bigcup1. +have [i Ei bip] := Op; exists i; split => //; first exact: ED. +by apply: subset_trans OA => q biq; exists i. +Qed. + +Lemma op_bigU (J : Type) (f : J -> set type) : + (forall i : J, open_of (f i)) -> open_of (\bigcup_i f i). +Proof. +move=> /choice [select selectP]; exists (imagei select setT). +split; first by move=> i [j _ sji]; have [/(_ _ sji)] := selectP j. +by rewrite bigcup_image; apply: eq_bigcupr => x _; have [] := selectP x. +Qed. + +Fact nbhs_of_openE : open_of = [set A : set type | A `<=` nbhs^~ A]. +Proof. +have -> : nbhs = fun p => Nbhs (base_nbhs p). (* reexpress [nbhs x | base_nbhs p] *) + by rewrite funeqE=> U; apply: in_nbhs_inj; rewrite nbhs_open. +by apply: OfOpen.nbhs_of_openE; apply: op_bigU. +Qed. + +Definition topologyMixin : Topological.mixin_of (nbhs : type -> set (set type)) := + Topological.Mixin nbhs_open nbhs_of_openE. +Canonical topologicalType := Eval hnf in TopologicalType type topologyMixin. + +End OfBase. +End OfBase. (** ** Topology defined by a subbase of open sets *) @@ -1611,57 +1881,101 @@ rewrite predeqE => t; split=> [|fit]; first by apply; rewrite in_fsetE. by move=> ?; rewrite in_fsetE => /eqP->. Qed. -Section TopologyOfSubbase. +Module OfSubbase. +Section OfSubbase. -Variable (I : pointedType) (T : Type) (D : set I) (b : I -> set T). +Variable (I : choiceType) (T : pointedType) (sD : set I) (sb : I -> set T). +Definition type : Type := T. -Program Definition topologyOfSubbaseMixin := - @topologyOfBaseMixin _ _ (finI_from D b) id (finI_from_cover D b) _. -Next Obligation. -move: i j t H H0 H1 H2 => A B t [DA sDAD AeIbA] [DB sDBD BeIbB] At Bt. -exists (A `&` B); split; last by split. -exists (DA `|` DB)%fset; first by move=> i /fsetUP [/sDAD|/sDBD]. -rewrite predeqE => s; split=> [Ifs|[As Bs] i /fsetUP]. - split; first by rewrite -AeIbA => i DAi; apply: Ifs; rewrite in_fsetE DAi. - by rewrite -BeIbB => i DBi; apply: Ifs; rewrite in_fsetE DBi orbC. -by move=> [DAi|DBi]; - [have := As; rewrite -AeIbA; apply|have := Bs; rewrite -BeIbB; apply]. +Notation D := (finI_from sD sb). +Definition b := (@id (set T)). +Notation nbhs_of := (OfBase.nbhs_of D b). +Notation open_of := (OfBase.open_of D b). + +Canonical pointedType := Eval hnf in [pointedType of type]. + +Definition nbhsMixin : Nbhs.mixin_of type type := NbhsMixin_ nbhs_of. +Canonical nbhsType := Eval hnf in NbhsType type type nbhsMixin. + +Let b_cover : \bigcup_(i in D) b i = setT. +Proof. exact: finI_from_cover. Qed. + +Let b_join : forall i j t, D i -> D j -> b i t -> b j t -> + exists k, [/\ D k, b k t & b k `<=` b i `&` b j]. +Proof. +move=> _ _ x [A AsD <-] [B BsD <-] bAx bBx. +exists (\bigcap_(i in [set i | i \in (A `|` B)%fset]) sb i); split. +- by exists (A `|` B)%fset => // y; rewrite inE => /orP[/AsD|/BsD]. +- by move=> y; rewrite inE => /orP[yA|yB]; [apply: bAx|apply: bBx]. +- move=> y b_y; split. + by move=> z zA; apply: b_y; rewrite inE zA. + by move=> z zB; apply: b_y; rewrite inE zB orbT. Qed. -End TopologyOfSubbase. +Lemma filterMixin : Filter.mixin_of [nbhsType type of type]. +Proof. by apply: OfBase.filterMixin; [apply: b_cover|apply: b_join]. Qed. +Canonical filterType := Eval hnf in FilterType type type filterMixin. + +Lemma pfilterMixin : PFilter.mixin_of [filterType type of type]. +Proof. by have [P] := (OfBase.pfilterMixin b_cover b_join); exists. Qed. +Canonical pfilterType := Eval hnf in PFilterType type type pfilterMixin. + +Notation base_nbhs p := [set A | exists B, [/\ open_of B, B p & B `<=` A]]. + +Definition topologyMixin : Topological.mixin_of (nbhs : type -> set (set type)) := + Topological.Mixin (OfBase.nbhs_open D b) (OfBase.nbhs_of_openE D b). +Canonical topologicalType := Eval hnf in TopologicalType type topologyMixin. + +End OfSubbase. +End OfSubbase. + (** ** Topology on the product of two spaces *) -Section Prod_Topology. -Context {T U : topologicalType}. +(** ** Topology on matrices *) -Let prod_loc (p : T * U) := filter_prod (locally p.1) (locally p.2). +Section MatrixNbhsType. +Context (m n : nat) {T : Type} (fT : nbhsType T). -Lemma prod_loc_filter (p : T * U) : ProperFilter (prod_loc p). -Proof. exact: filter_prod_proper. Qed. +Definition mx_filter (mx : 'M[fT]_(m, n)) : set (set 'M[T]_(m,n)) := + nbhs_from [set P | forall i j, (nbhs (mx i j)) (P i j)] + (fun P => [set my : 'M[T]_(m, n) | forall i j, P i j (my i j)]). -Lemma prod_loc_singleton (p : T * U) (A : set (T * U)) : prod_loc p A -> A p. -Proof. -by move=> [QR [/locally_singleton Qp1 /locally_singleton Rp2]]; apply. -Qed. +Definition mx_nbhs_mixin := NbhsMixin_ mx_filter. -Lemma prod_loc_loc (p : T * U) (A : set (T * U)) : - prod_loc p A -> prod_loc p (prod_loc^~ A). +Canonical mx_nbhs := Eval hnf in NbhsType 'M[T]_(m,n) 'M[fT]_(m,n) mx_nbhs_mixin. +End MatrixNbhsType. + +Section MatrixFilter. +Context (m n : nat) {T : Type} (fT : filterType T). + +Lemma mx_filter_mixin : + Filter.mixin_of [nbhsType 'M[T]_(m, n) of 'M[fT]_(m, n)]. Proof. -move=> [QR [/locally_interior p1_Q /locally_interior p2_R] sQRA]. -by exists (QR.1^°, QR.2^°) => // ??; exists QR. +constructor=> /= M; apply: nbhs_from_filter => [|A B AM BM]. + by exists (fun _ _ => setT) => i j; apply: nearT. +exists (fun i j => A i j `&` B i j) => [i j|]. + by move: (AM i j) (BM i j); apply: nearS2. +by move=> M' ABM'; split=> i j; move: (ABM' i j) => []. Qed. -Definition prod_topologicalTypeMixin := - topologyOfFilterMixin prod_loc_filter prod_loc_singleton prod_loc_loc. +Canonical mx_filtered := Eval hnf in FilterType 'M[T]_(m,n) 'M[fT]_(m,n) mx_filter_mixin. +End MatrixFilter. -Canonical prod_topologicalType := - TopologicalType (T * U) prod_topologicalTypeMixin. +Section MatrixPFilter. +Context (m n : nat) {T : pointedType} (fT : pfilterType T). -End Prod_Topology. +Lemma mx_pfilter_mixin : + PFilter.mixin_of [filterType 'M[T]_(m, n) of 'M[fT]_(m, n)]. +Proof. +constructor=> /= M [A AF]. +have /choice [f /(_ (_,_))/= fP] := fun ij => near_ex (uncurry_dep AF ij). +by move=> /(_ (\matrix_(i,j) f (i, j))); apply=> i j; rewrite mxE; apply: fP. +Qed. -(** ** Topology on matrices *) +Canonical mx_pfiltered := Eval hnf in PFilterType 'M[T]_(m,n) 'M[fT]_(m,n) mx_pfilter_mixin. +End MatrixPFilter. Section matrix_Topology. @@ -1669,31 +1983,21 @@ Variables (m n : nat) (T : topologicalType). Implicit Types M : 'M[T]_(m, n). -Lemma mx_loc_filter M : ProperFilter (locally M). -Proof. -apply: (filter_from_proper (filter_from_filter _ _)) => [|P Q M_P M_Q|P M_P]. -- by exists (fun i j => setT) => ??; apply: filterT. -- exists (fun i j => P i j `&` Q i j) => [??|mx PQmx]; first exact: filterI. - by split=> i j; have [] := PQmx i j. -- exists (\matrix_(i, j) get (P i j)) => i j; rewrite mxE; apply: getPex. - exact: filter_ex (M_P i j). -Qed. - -Lemma mx_loc_singleton M (A : set 'M[T]_(m, n)) : locally M A -> A M. -Proof. by move=> [P M_P]; apply=> ??; apply: locally_singleton. Qed. +Lemma mx_loc_singleton M (A : set 'M[T]_(m, n)) : nbhs M A -> A M. +Proof. by move=> [P M_P]; apply=> ? ?; apply: nbhs_singleton. Qed. Lemma mx_loc_loc M (A : set 'M[T]_(m, n)) : - locally M A -> locally M (locally^~ A). + nbhs M A -> nbhs M (nbhs^~ A). Proof. move=> [P M_P sPA]; exists (fun i j => (P i j)^°). - by move=> ??; apply: locally_interior. -by move=> ??; exists P. + by move=> ? ?; apply: nbhs_interior. +by move=> ? ?; exists P. Qed. Definition matrix_topologicalTypeMixin := - topologyOfFilterMixin mx_loc_filter mx_loc_singleton mx_loc_loc. + topologyOfFilterMixin mx_loc_singleton mx_loc_loc. -Canonical matrix_topologicalType := +Canonical matrix_topologicalType := Eval hnf in TopologicalType 'M[T]_(m, n) matrix_topologicalTypeMixin. End matrix_Topology. @@ -1702,8 +2006,11 @@ End matrix_Topology. Section Weak_Topology. +Definition weak_topology {S T : Type} (f : S -> T) := S. Variable (S : pointedType) (T : topologicalType) (f : S -> T). +Notation fweak := (weak_topology f). + Definition wopen := [set f @^-1` A | A in open]. Lemma wopT : wopen setT. @@ -1728,28 +2035,32 @@ rewrite predeqE => s; split=> [[i _]|[i _]]; last by rewrite g_preim; exists i. by rewrite -[_ _]/((f @^-1` _) _) -g_preim; exists i. Qed. -Definition weak_topologicalTypeMixin := topologyOfOpenMixin wopT wopI wop_bigU. - -Let S_filteredClass := Filtered.Class (Pointed.class S) (locally_of_open wopen). -Definition weak_topologicalType := - Topological.Pack (@Topological.Class _ S_filteredClass - weak_topologicalTypeMixin) S. +Canonical weak_pointedType := Eval hnf in [pointedType of fweak]. +Definition weak_nbhsMixin := OfOpen.nbhsMixin wopen. +Canonical weak_nbhsType := Eval hnf in NbhsType fweak fweak weak_nbhsMixin. +Definition weak_filterMixin := OfOpen.filterMixin wopT wopI. +Canonical weak_filterType := Eval hnf in FilterType fweak fweak weak_filterMixin. +Definition weak_pfilterMixin := OfOpen.pfilterMixin wopT wopI. +Canonical weak_pfilterType := Eval hnf in PFilterType fweak fweak weak_pfilterMixin. +Definition weak_topologyMixin := OfOpen.topologyMixin wop_bigU. +Canonical weak_topologyType := Eval hnf in TopologicalType fweak weak_topologyMixin. -Lemma weak_continuous : continuous (f : weak_topologicalType -> T). +Lemma weak_continuous : continuous (f : fweak -> T). Proof. by apply/continuousP => A ?; exists A. Qed. -Lemma flim_image (F : set (set S)) (s : S) : - Filter F -> f @` setT = setT -> - F --> (s : weak_topologicalType) <-> [set f @` A | A in F] --> (f s). +Lemma cvg_image (F : {filter S}) (s : fweak) : + f @` setT = setT -> + F --> s <-> [set f @` A | A in F] --> f s. Proof. -move=> FF fsurj; split=> [cvFs|cvfFfs]. - move=> A /weak_continuous [B [Bop [Bs sBAf]]]. - have /cvFs FB: locally (s : weak_topologicalType) B by apply: neigh_locally. - rewrite locally_simpl; exists (f @^-1` A); first exact: filterS FB. +move=> fsurj; split=> [cvFs|cvfFfs]. + move=> A /weak_continuous [B [Bop Bs sBAf]]. + have /cvFs FB: nbhs s B by apply: neigh_nbhs. + exists (f @^-1` A); first exact: nearS FB. exact: image_preimage. -move=> A /= [_ [[B Bop <-] [Bfs sBfA]]]. -have /cvfFfs [C FC fCeB] : locally (f s) B by rewrite locallyE; exists B; split. -rewrite locally_filterE; apply: filterS FC. +move=> A /= [_ [[B Bop <-]]/= Bfs sBfA]. +have /cvfFfs [C FC fCeB] : nbhs (f s) B. + by rewrite open_nbhsE; exists B; split. +apply: nearS (FC : nbhs F C). by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image. Qed. @@ -1757,101 +2068,101 @@ End Weak_Topology. (** ** Supremum of a family of topologies *) -Section Sup_Topology. +(* Section Sup_Topology. *) -Variable (T : pointedType) (I : Type) (Tc : I -> Topological.class_of T). +(* Variable (T : pointedType) (I : Type) (Tc : I -> Topological.class_of T). *) -Let TS := fun i => Topological.Pack (Tc i) T. +(* Let TS := fun i => Topological.Pack (Tc i) T. *) -Definition sup_subbase := \bigcup_i (@open (TS i) : set (set T)). +(* Definition sup_subbase := \bigcup_i (@open (TS i) : set (set T)). *) -Definition sup_topologicalTypeMixin := topologyOfSubbaseMixin sup_subbase id. +(* Definition sup_topologicalTypeMixin := OfSubbase.topologyMixin sup_subbase id. *) -Definition sup_topologicalType := - Topological.Pack (@Topological.Class _ (Filtered.Class (Pointed.class T) _) - sup_topologicalTypeMixin) T. +(* Definition sup_topologicalType := Topological.Pack *) +(* (@Topological.Class _ *) +(* (@PFilter.Class _ _ *) +(* (@Filter.Class _ _ *) +(* (Nbhs.Class (Pointed.class T) _) _) _) *) +(* sup_topologicalTypeMixin) T. *) -Lemma flim_sup (F : set (set T)) (t : T) : - Filter F -> F --> (t : sup_topologicalType) <-> forall i, F --> (t : TS i). -Proof. -move=> Ffilt; split=> cvFt. - move=> i A /=; rewrite (@locallyE (TS i)) => - [B [[Bop Bt] sBA]]. - apply: cvFt; exists B; split=> //; exists [set B]; last first. - by rewrite predeqE => ?; split=> [[_ ->]|] //; exists B. - move=> _ ->; exists [fset B]%fset. - by move=> ?; rewrite in_fsetE in_setE => /eqP->; exists i. - by rewrite predeqE=> ?; split=> [|??]; [apply|]; rewrite in_fsetE // =>/eqP->. -move=> A /=; rewrite (@locallyE sup_topologicalType). -move=> [_ [[[B sB <-] [C BC Ct]] sUBA]]. -rewrite locally_filterE; apply: filterS sUBA _; apply: (@filterS _ _ _ C). - by move=> ??; exists C. -have /sB [D sD IDeC] := BC; rewrite -IDeC; apply: filter_bigI => E DE. -have /sD := DE; rewrite in_setE => - [i _]; rewrite openE => Eop. -by apply: (cvFt i); apply: Eop; move: Ct; rewrite -IDeC => /(_ _ DE). -Qed. +(* Lemma cvg_sup (F : {filter T}) (t : T) : *) +(* F --> (t : sup_topologicalType) <-> forall i, F --> (t : TS i). *) +(* Proof. *) +(* move=> Ffilt; split=> cvFt. *) +(* move=> i A /=; rewrite (@nbhsE (TS i)) => - [B [[Bop Bt] sBA]]. *) +(* apply: cvFt; exists B; split=> //; exists [set B]; last first. *) +(* by rewrite predeqE => ?; split=> [[_ ->]|] //; exists B. *) +(* move=> _ ->; exists [fset B]%fset. *) +(* by move=> ?; rewrite in_fsetE in_setE => /eqP->; exists i. *) +(* by rewrite predeqE=> ?; split=> [|? ?]; [apply|]; rewrite in_fsetE // =>/eqP->. *) +(* move=> A /=; rewrite (@nbhsE sup_topologicalType). *) +(* move=> [_ [[[B sB <-] [C BC Ct]] sUBA]]. *) +(* rewrite nbhs_filterE; apply: nearS sUBA _; apply: (@nearS _ _ _ C). *) +(* by move=> ? ?; exists C. *) +(* have /sB [D sD IDeC] := BC; rewrite -IDeC; apply: filter_bigI => E DE. *) +(* have /sD := DE; rewrite in_setE => - [i _]; rewrite openE => Eop. *) +(* by apply: (cvFt i); apply: Eop; move: Ct; rewrite -IDeC => /(_ _ DE). *) +(* Qed. *) -End Sup_Topology. +(* End Sup_Topology. *) -(** ** Product topology *) +(* (** ** Product topology *) *) -Section Product_Topology. +(* Section Product_Topology. *) -Variable (I : Type) (T : I -> topologicalType). +(* Variable (I : Type) (T : I -> topologicalType). *) -Definition dep_arrow_choiceClass := - Choice.Class (Equality.class (dep_arrow_eqType T)) gen_choiceMixin. +(* Definition dep_arrow_choiceClass := *) +(* Choice.Class (Equality.class (dep_arrow_eqType T)) gen_choiceMixin. *) -Definition dep_arrow_pointedType := - Pointed.Pack (Pointed.Class dep_arrow_choiceClass (fun i => @point (T i))) - (forall i, T i). +(* Definition dep_arrow_pointedType := *) +(* Pointed.Pack (Pointed.Class dep_arrow_choiceClass (fun i => @point (T i))) *) +(* (forall i, T i). *) -Definition product_topologicalType := - sup_topologicalType (fun i => Topological.class - (weak_topologicalType (fun f : dep_arrow_pointedType => f i))). +(* Definition product_topologicalType := *) +(* sup_topologicalType (fun i => Topological.class *) +(* (weak_topologicalType (fun f : dep_arrow_pointedType => f i))). *) -End Product_Topology. +(* End Product_Topology. *) (** * The topology on natural numbers *) (* :TODO: ultimately nat could be replaced by any lattice *) -Definition eventually := filter_from setT (fun N => [set n | (N <= n)%N]). +Definition eventually := nbhs_from setT (fun N => [set n | (N <= n)%N]). Notation "'\oo'" := eventually : classical_set_scope. -Canonical eventually_filter_source X := - @Filtered.Source X _ nat (fun f => f @ \oo). +Canonical eventually_filter_source X := Eval hnf in + @Nbhs.Source X _ nat (NbhsMixin_ (fun f => f @ \oo)). -Global Instance eventually_filter : ProperFilter eventually. +Definition eventually_filter : is_pfilter eventually. Proof. -eapply @filter_from_proper; last by move=> i _; exists i. -apply: filter_fromT_filter; first by exists 0%N. +apply: nbhs_from_proper; last by move=> i _; exists i. +apply: nbhs_fromT_filter; first by exists 0%N. move=> i j; exists (maxn i j) => n //=. by rewrite geq_max => /andP[ltin ltjn]. Qed. -(** locally' *) +(** nbhs' *) (* Should have a generic ^' operator *) -Definition locally' {T : topologicalType} (x : T) := - within (fun y => y != x) (locally x). +Definition nbhs' {T : topologicalType} (x : T) := + within (fun y => y != x) x. -Lemma locallyE' (T : topologicalType) (x : T) : - locally x = locally' x `&` at_point x. +Lemma nbhsE' (T : topologicalType) (x : T) : + nbhs x = nbhs' x `&` at_point x :> set _. Proof. rewrite predeqE => A; split=> [x_A|[x_A Ax]]. - split; last exact: locally_singleton. - move: x_A; rewrite locallyE => -[B [x_B sBA]]; rewrite /locally' locallyE. - by exists B; split=> // ? /sBA. -move: x_A; rewrite /locally' !locallyE => -[B [x_B sBA]]; exists B. -by split=> // y /sBA Ay; case: (eqVneq y x) => [->|]. -Qed. + by split; [by near=> y => _; near: y|exact: nbhs_singleton]. +by near=> y; have [->//|] := eqVneq y x; near: y. +Grab Existential Variables. all: end_near. Qed. -Global Instance locally'_filter {T : topologicalType} (x : T) : - Filter (locally' x). +Definition nbhs'_is_filter {T : topologicalType} (x : T) : + is_filter (nbhs (nbhs' x)). Proof. exact: within_filter. Qed. -Typeclasses Opaque locally'. +Typeclasses Opaque nbhs'. -Canonical locally'_filter_on (T : topologicalType) (x : T) := - FilterType (locally' x) (locally'_filter _). +Canonical nbhs'_filter_on (T : topologicalType) (x : T) := Eval hnf in + Filter (nbhs' x) (nbhs'_is_filter _). (** ** Closed sets in topological spaces *) @@ -1860,10 +2171,10 @@ Section Closed. Context {T : topologicalType}. Definition closure (A : set T) := - [set p : T | forall B, locally p B -> A `&` B !=set0]. + [set p : T | forall B, nbhs p B -> A `&` B !=set0]. Lemma subset_closure (A : set T) : A `<=` closure A. -Proof. by move=> p ??; exists p; split=> //; apply: locally_singleton. Qed. +Proof. by move=> p ? ?; exists p; split=> //; apply: nbhs_singleton. Qed. Lemma closureI (A B : set T) : closure (A `&` B) `<=` closure A `&` closure B. Proof. by move=> p clABp; split=> ? /clABp [q [[]]]; exists q. Qed. @@ -1889,29 +2200,21 @@ Qed. Lemma closedT : closed setT. Proof. by []. Qed. Lemma closed0 : closed set0. -Proof. by move=> ? /(_ setT) [|? []] //; apply: filterT. Qed. +Proof. by move=> ? /(_ setT) [|? []] //; apply: nearT. Qed. Lemma closedE : closed = [set A : set T | forall p, ~ (\near p, ~ A p) -> A p]. Proof. rewrite predeqE => A; split=> Acl p; last first. - by move=> clAp; apply: Acl; rewrite -locally_nearE => /clAp [? []]. -rewrite -locally_nearE locallyE => /asboolP. -rewrite asbool_neg => /forallp_asboolPn clAp. -apply: Acl => B; rewrite locallyE => - [C [p_C sCB]]. -have /asboolP := clAp C. -rewrite asbool_neg asbool_and => /nandP [/asboolP//|/existsp_asboolPn [q]]. -move/asboolP; rewrite asbool_neg => /imply_asboolPn [/sCB Bq /contrapT Aq]. -by exists q. -Qed. + by move=> clAp; apply: Acl => /clAp [? []]. +move=> NAp; apply: Acl => Q Qx; apply: contrapNT NAp => NAQ. +by near=> x; apply: contrapNN NAQ => Ax; exists x; split=> //; near: x. +Grab Existential Variables. all: end_near. Qed. Lemma openC (D : set T) : closed D -> open (~` D). -Proof. -rewrite closedE openE => Dcl t nDt; apply: contrapT. -by rewrite /interior locally_nearE => /Dcl. -Qed. +Proof. by rewrite closedE openE => Dcl t nDt; apply: contrapT => /Dcl. Qed. Lemma closed_closure (A : set T) : closed (closure A). -Proof. by move=> p clclAp B /locally_interior /clclAp [q [clAq /clAq]]. Qed. +Proof. by move=> p clclAp B /nbhs_interior /clclAp [q [clAq /clAq]]. Qed. End Closed. @@ -1920,24 +2223,22 @@ Lemma closed_comp {T U : topologicalType} (f : T -> U) (D : set U) : Proof. rewrite !closedE=> f_cont D_cl x /= xDf; apply: D_cl; apply: contrap xDf => fxD. have NDfx : ~ D (f x). - by move: fxD; rewrite -locally_nearE locallyE => - [A [[??]]]; apply. + by move: fxD; rewrite open_nbhsE => - [A [[? ?]]]; apply. by apply: f_cont fxD; rewrite in_setE. Qed. -Lemma closed_flim_loc {T} {U : topologicalType} {F} {FF : ProperFilter F} +Lemma closed_cvg_loc {T} {U : topologicalType} {F : {pfilter T}} (f : T -> U) (D : U -> Prop) : - forall y, f @ F --> y -> F (f @^-1` D) -> closed D -> D y. + forall y, f @ F --> y -> nbhs F (f @^-1` D) -> closed D -> D y. Proof. -move=> y Ffy Df; apply => A /Ffy /=; rewrite locally_filterE. -by move=> /(filterI Df); apply: filter_ex. -Qed. +move=> y Ffy/= Df; apply => A /Ffy /=; rewrite nearE/= => Af. +by near F => x; exists (f x); split; near: x. +Grab Existential Variables. all: end_near. Qed. -Lemma closed_flim {T} {U : topologicalType} {F} {FF : ProperFilter F} +Lemma closed_cvg {T} {U : topologicalType} {F : {pfilter T}} (f : T -> U) (D : U -> Prop) : forall y, f @ F --> y -> (forall x, D (f x)) -> closed D -> D y. -Proof. -by move=> y fy FDf; apply: (closed_flim_loc fy); apply: filterE. -Qed. +Proof. by move=> y fy FDf; apply: (closed_cvg_loc fy); apply: nearW. Qed. (** ** Compact sets *) @@ -1946,198 +2247,290 @@ Section Compact. Context {T : topologicalType}. Definition cluster (F : set (set T)) (p : T) := - forall A B, F A -> locally p B -> A `&` B !=set0. + forall A B, F A -> nbhs p B -> A `&` B !=set0. Lemma clusterE F : cluster F = \bigcap_(A in F) (closure A). -Proof. by rewrite predeqE => p; split=> cF ????; apply: cF. Qed. +Proof. by rewrite predeqE => p; split=> cF ? ? ? ?; apply: cF. Qed. -Lemma flim_cluster F G : F --> G -> cluster F `<=` cluster G. +Lemma cvg_cluster F G : F --> G -> cluster F `<=` cluster G. Proof. by move=> sGF p Fp P Q GP Qp; apply: Fp Qp; apply: sGF. Qed. -Lemma cluster_flimE F : - ProperFilter F -> - cluster F = [set p | exists2 G, ProperFilter G & G --> p /\ F `<=` G]. +Lemma cluster_cvgE (fT : pfilterType T) {F : fT} : + cluster (nbhs F) = [set p | exists2 G : {pfilter T}, G --> p & G --> F]. Proof. -move=> FF; rewrite predeqE => p. -split=> [clFp|[G Gproper [cvGp sFG]] A B]; last first. - by move=> /sFG GA /cvGp GB; apply: (@filter_ex _ G); apply: filterI. -exists (filter_from (\bigcup_(A in F) [set A `&` B | B in locally p]) id). - apply filter_from_proper; last first. +rewrite predeqE => p. +split=> [clFp|[G cvGp sFG] A B]; last first. + by move=> /sFG GA /cvGp GB; near G => x; exists x; split; near: x. +pose Gbody := nbhs_from (\bigcup_(A in nbhs F) [set A `&` B | B in nbhs p]) id. +have Gpf : is_pfilter Gbody. + apply: nbhs_from_proper => /=; last first. by move=> _ [A FA [B p_B <-]]; have := clFp _ _ FA p_B. - apply: filter_from_filter. - exists setT; exists setT; first exact: filterT. - by exists setT; [apply: filterT|rewrite setIT]. + apply: nbhs_from_filter. + exists setT, setT; first exact: nearT. + by exists setT; [apply: nearT|rewrite setIT]. move=> _ _ [A1 FA1 [B1 p_B1 <-]] [A2 FA2 [B2 p_B2 <-]]. - exists (A1 `&` B1 `&` (A2 `&` B2)) => //; exists (A1 `&` A2). - exact: filterI. - by exists (B1 `&` B2); [apply: filterI|rewrite setIACA]. -split. - move=> A p_A; exists A => //; exists setT; first exact: filterT. + exists (A1 `&` B1 `&` (A2 `&` B2)) => //. + exists (A1 `&` A2); first exact: nearI. + by exists (B1 `&` B2); [apply: nearI|rewrite setIACA]. +pose G := PFilterPack Gbody Gpf. +exists G. + move=> A p_A; exists A => //; exists setT; first exact: nearT. by exists A => //; rewrite setIC setIT. -move=> A FA; exists A => //; exists A => //; exists setT; first exact: filterT. +move=> A FA; do 2!exists A => //; exists setT; first exact: nearT. by rewrite setIT. -Qed. +Grab Existential Variables. all: end_near. Qed. -Definition compact A := forall (F : set (set T)), - ProperFilter F -> F A -> A `&` cluster F !=set0. +Definition compact A := forall (fT : pfilterType T) (F : fT), + nbhs F A -> A `&` cluster (nbhs F) !=set0. Lemma compact0 : compact set0. -Proof. by move=> F FF /filter_ex []. Qed. +Proof. by move=> fT F /near_ex []. Qed. Lemma subclosed_compact (A B : set T) : closed A -> compact B -> A `<=` B -> compact A. Proof. -move=> Acl Bco sAB F Fproper FA. -have [|p [Bp Fp]] := Bco F; first exact: filterS FA. +move=> Acl Bco sAB fT F FA. +have [|p [Bp Fp]] := Bco _ F; first exact: nearS FA. by exists p; split=> //; apply: Acl=> C Cp; apply: Fp. Qed. -Definition hausdorff := forall p q : T, cluster (locally p) q -> p = q. +Definition hausdorff := forall p q : T, cluster (nbhs p) q -> p = q. -Typeclasses Opaque within. -Global Instance within_locally_proper (A : set T) p : - infer (closure A p) -> ProperFilter (within A (locally p)). +Definition within_nbhs_proper (A : set T) p : + (closure A p) -> is_pfilter (within A p). Proof. -move=> clAp; apply: Build_ProperFilter => B. -by move=> /clAp [q [Aq AqsoBq]]; exists q; apply: AqsoBq. +move=> clAp; apply: Build_is_pfilter; last exact: filter_class. +by move=> P /clAp [q [Aq AqsoBq]]; exists q; apply: AqsoBq. Qed. Lemma compact_closed (A : set T) : hausdorff -> compact A -> closed A. Proof. -move=> hT Aco p clAp; have pA := !! @withinT _ (locally p) A _. -have [q [Aq clsAp_q]] := !! Aco _ _ pA; rewrite (hT p q) //. -by apply: flim_cluster clsAp_q; apply: flim_within. +move=> hT Aco p clAp; have := @withinT _ _ A p. +case: pfilterP => [|w eqw]; first exact: within_nbhs_proper. +move=> /(Aco _ w)[q [Aq clsAp_q]]; rewrite (hT p q) //. +by apply: cvg_cluster clsAp_q; rewrite eqw; apply: cvg_within. Qed. End Compact. Arguments hausdorff : clear implicits. +Arguments pfilterP {_ _}. Lemma continuous_compact (T U : topologicalType) (f : T -> U) A : {in A, continuous f} -> compact A -> compact (f @` A). Proof. -move=> fcont Aco F FF FfA; set G := filter_from F (fun C => A `&` f @^-1` C). -have GF : ProperFilter G. - apply: (filter_from_proper (filter_from_filter _ _)); first by exists (f @` A). - move=> C1 C2 F1 F2; exists (C1 `&` C2); first exact: filterI. +move=> fcont Aco fT F FfA. +have [|G eqG] := pfilterP (nbhs_from (nbhs F) (fun C => A `&` f @^-1` C)). + apply: (nbhs_from_proper (nbhs_from_filter _ _)); first by exists (f @` A). + move=> C1 C2 F1 F2; exists (C1 `&` C2); first exact: nearI. by move=> ?[?[]]; split; split. - by move=> C /(filterI FfA) /filter_ex [_ [[p ? <-]]]; eexists p. -case: (Aco G); first by exists (f @` A) => // ? []. + by move=> C /(nearI FfA) /near_ex [_ [[p ? <-]]]; eexists p. +case: (Aco _ G); first by rewrite eqG; exists (f @` A) => // ? []. move=> p [Ap clsGp]; exists (f p); split; first exact/imageP. -move=> B C FB /fcont; rewrite in_setE /= locally_filterE => /(_ Ap) p_Cf. -have : G (A `&` f @^-1` B) by exists B. +move=> B C FB /fcont; rewrite in_setE /= => /(_ Ap) p_Cf. +have : G (A `&` f @^-1` B) by rewrite eqG; exists B. by move=> /clsGp /(_ p_Cf) [q [[]]]; exists (f q). Qed. Section Tychonoff. -Class UltraFilter T (F : set (set T)) := { - ultra_proper :> ProperFilter F ; - max_filter : forall G : set (set T), ProperFilter G -> F `<=` G -> G = F +Definition filter_is_ultra T (F : set (set T)) := + forall G : pfilter_on T, F `<=` G -> G = F :> set _. + +Record is_ufilter T (F : set (set T)) := { + pfilter_ufilter :> is_pfilter F ; + _ : filter_is_ultra F }. -Lemma ultra_flim_clusterE (T : topologicalType) (F : set (set T)) : - UltraFilter F -> cluster F = [set p | F --> p]. -Proof. -move=> FU; rewrite predeqE => p; split. - by rewrite cluster_flimE => - [G GF [cvGp /max_filter <-]]. -by move=> cvFp; rewrite cluster_flimE; exists F; [apply: ultra_proper|split]. -Qed. +Structure ufilter_on T := UFilterPack { + in_ufilter :> set (set T); + _ : is_ufilter in_ufilter +}. -Lemma ultraFilterLemma T (F : set (set T)) : - ProperFilter F -> exists G, UltraFilter G /\ F `<=` G. -Proof. -move=> FF. -set filter_preordset := ({G : set (set T) & ProperFilter G /\ F `<=` G}). +Definition ufilter_class T (F : ufilter_on T) : is_ufilter F := + let: UFilterPack _ class := F in class. +Arguments UFilterPack {T} _ _. +Canonical ufilter_nbhs_on T (F : ufilter_on T) := Eval hnf in Nbhs F. +Coercion ufilter_nbhs_on : ufilter_on >-> nbhs_on. +Canonical ufilter_filter_on T (F : ufilter_on T) := + Eval hnf in Filter F (ufilter_class F). +Coercion ufilter_filter_on : ufilter_on >-> filter_on. +Canonical ufilter_pfilter_on T (F : ufilter_on T) := + Eval hnf in PFilterPack F (ufilter_class F). +Coercion ufilter_pfilter_on : ufilter_on >-> pfilter_on. + +Definition UFilter_of {T} (F : set (set T)) (ultraF : filter_is_ultra F) := + fun (fF : pfilter_on T) of phant_id F (fF : set (set T)) => + fun (fFF : is_pfilter _) of phant_id (PFilterPack _ fFF) fF => + UFilterPack F (Build_is_ufilter fFF ultraF). +Notation UFilter F ultraF := (@UFilter_of _ F ultraF _ id _ id). + +Lemma ultra_pointfilter (T : pointedType) (x : T) : + filter_is_ultra (pointfilter x). +Proof. +rewrite /pointfilter/= => G pG; rewrite predeqE => A; split => [|/pG//]. +rewrite -nbhs_setE => GA; have Gp : G [set x] by apply: pG. +by near G => y; suff <- : y = x; near: y. +Grab Existential Variables. all: end_near. Qed. + +Lemma ufilter_is_pfilter (T : Type) (pT : ufilter_on T) : + filter_is_proper (Nbhs (in_ufilter pT)). +Proof. by case: pT => ? [[]]. Qed. + +Lemma ufilter_is_filter (T : Type) (pT : ufilter_on T) : + is_filter (Nbhs (in_pfilter pT)). +Proof. exact: pfilter_is_filter. Qed. + +Canonical ufilter_on_eqType T := Eval hnf in EqType (ufilter_on T) gen_eqMixin. +Canonical ufilter_on_choiceType T := Eval hnf in + ChoiceType (ufilter_on T) gen_choiceMixin. +Canonical pointfilter_ufilter (T : pointedType) (x : T) := Eval hnf in + UFilter (pointfilter x) (@ultra_pointfilter _ x). +Canonical ufilter_on_PointedType (T : pointedType) := Eval hnf in + PointedType (ufilter_on T) (pointfilter_ufilter point). +Definition ufilter_on_nbhs_mixin (T : pointedType) := + NbhsMixin_ (@in_ufilter T). +Canonical ufilter_on_nbhsType (T : pointedType) := Eval hnf in + NbhsType T (ufilter_on T) (@ufilter_on_nbhs_mixin T). +Definition ufilter_on_filter_mixin (T : pointedType) := + FilterMixin (@ufilter_is_filter T). +Canonical ufilter_on_filterType (T : pointedType) := Eval hnf in + FilterType T (ufilter_on T) (@ufilter_on_filter_mixin T). +Definition ufilter_on_pfilter_mixin (T : pointedType) := + PFilterMixin (@ufilter_is_pfilter T). +Canonical ufilter_on_pfilterType (T : pointedType) := Eval hnf in + PFilterType T (ufilter_on T) (@ufilter_on_pfilter_mixin T). + +Notation "{ 'ufilter' T }" := (ufilter_on_nbhsType T) + (at level 0, format "{ 'ufilter' T }" ) : type_scope. + +Lemma ufilter_on_pfilter (T : Type) (F : ufilter_on T) : + ~ (in_ufilter F) set0. +Proof. by case: F => /= F [[]]. Qed. + +Lemma max_filter (T : pointedType) (F : {ufilter T}) : + forall G : {pfilter T}, F `<=` G -> G = F. +Proof. +case: F => /= F [Fp Fu] [G Gp] /Fu eqGF. +case: _ / eqGF Fp Fu => /= Fp Fu; suff -> : Gp = Fp by []. +exact: Prop_irrelevance. +Qed. + +Lemma ultra_cvg_clusterE (T : topologicalType) (F : ufilter_on T) : + cluster (nbhs F) = [set p | nbhs F --> p]. +Proof. +rewrite predeqE => p; split; last first. + by move=> cvFp; rewrite cluster_cvgE; exists (F : pfilter_on T). +rewrite cluster_cvgE => - [G cvGp /max_filter eqGF]. +by rewrite eqGF in cvGp. +Qed. + +Lemma mk_ufilter_subdef T (F : {pfilter T}) : + exists G : ufilter_on T, F `<=` G. +Proof. +set filter_preordset := ({G : {filter T} & is_pfilter G /\ F `<=` G}). set preorder := fun G1 G2 : filter_preordset => projT1 G1 `<=` projT1 G2. suff [G Gmax] : exists G : filter_preordset, premaximal preorder G. - have [GF sFG] := projT2 G; exists (projT1 G); split=> //; split=> // H HF sGH. - have sFH : F `<=` H by apply: subset_trans sGH. - have sHG : preorder (existT _ H (conj HF sFH)) G by apply: Gmax. - by rewrite predeqE => ?; split=> [/sHG|/sGH]. -have sFF : F `<=` F by []. -apply: (ZL_preorder ((existT _ F (conj FF sFF)) : filter_preordset)) => - [?|G H I sGH sHI ? /sGH /sHI|A Atot] //. -case: (pselect (A !=set0)) => [[G AG] | A0]; last first. - exists (existT _ F (conj FF sFF)) => G AG. - by have /asboolP := A0; rewrite asbool_neg => /forallp_asboolPn /(_ G). -have [GF sFG] := projT2 G. -suff UAF : ProperFilter (\bigcup_(H in A) projT1 H). - have sFUA : F `<=` \bigcup_(H in A) projT1 H. - by move=> B FB; exists G => //; apply: sFG. - exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH B HB /=. - by exists H. -apply Build_ProperFilter. - by move=> B [H AH HB]; have [HF _] := projT2 H; apply: (@filter_ex _ _ HF). -split; first by exists G => //; apply: filterT. - move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC. - exists HC => //; have [HCF _] := projT2 HC; apply: filterI HCC. - exact: sHBC. - exists HB => //; have [HBF _] := projT2 HB; apply: filterI HBB _. - exact: sHCB. -move=> B C SBC [H AH HB]; exists H => //; have [HF _] := projT2 H. -exact: filterS HB. -Qed. +(* have [GF sFG] := projT2 G; exists (projT1 G). split=> //; split=> // H HF sGH. *) +(* have sFH : F `<=` H by apply: subset_trans sGH. *) +(* have sHG : preorder (existT _ H (conj HF sFH)) G by apply: Gmax. *) +(* by rewrite predeqE => ?; split=> [/sHG|/sGH]. *) +(* have sFF : F `<=` F by []. *) +(* apply: (ZL_preorder ((existT _ F (conj FF sFF)) : filter_preordset)) => *) +(* [?|G H I sGH sHI ? /sGH /sHI|A Atot] //. *) +(* case: (pselect (A !=set0)) => [[G AG] | A0]; last first. *) +(* exists (existT _ F (conj FF sFF)) => G AG. *) +(* by have /asboolP := A0; rewrite asbool_neg => /forallp_asboolPn /(_ G). *) +(* have [GF sFG] := projT2 G. *) +(* suff UAF : is_pfilter (\bigcup_(H in A) projT1 H). *) +(* have sFUA : F `<=` \bigcup_(H in A) projT1 H. *) +(* by move=> B FB; exists G => //; apply: sFG. *) +(* exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH B HB /=. *) +(* by exists H. *) +(* apply Build_is_pfilter. *) +(* by move=> B [H AH HB]; have [HF _] := projT2 H; apply: (@near_ex _ _ HF). *) +(* split; first by exists G => //; apply: nearT. *) +(* move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC. *) +(* exists HC => //; have [HCF _] := projT2 HC; apply: nearI HCC. *) +(* exact: sHBC. *) +(* exists HB => //; have [HBF _] := projT2 HB; apply: nearI HBB _. *) +(* exact: sHCB. *) +(* move=> B C SBC [H AH HB]; exists H => //; have [HF _] := projT2 H. *) +(* exact: nearS HB. *) +(* Qed. *) +Admitted. Lemma compact_ultra (T : topologicalType) : - compact = [set A | forall F : set (set T), - UltraFilter F -> F A -> A `&` [set p | F --> p] !=set0]. -Proof. -rewrite predeqE => A; split=> Aco F FF FA. - by have /Aco [p [?]] := FA; rewrite ultra_flim_clusterE; exists p. -have [G [GU sFG]] := ultraFilterLemma FF. -have /Aco [p [Ap]] : G A by apply: sFG. -rewrite -[_ --> p]/([set _ | _] p) -ultra_flim_clusterE. -by move=> /(flim_cluster sFG); exists p. -Qed. + compact = [set A | forall F : ufilter_on T, + F A -> A `&` [set p | F --> p] !=set0]. +Proof. +(* rewrite predeqE => A; split=> Aco F FF FA. *) +(* by have /Aco [p [?]] := FA; rewrite ultra_cvg_clusterE; exists p. *) +(* have [G [GU sFG]] := ultrais_filterLemma FF. *) +(* have /Aco [p [Ap]] : G A by apply: sFG. *) +(* rewrite -[_ --> p]/([set _ | _] p) -ultra_cvg_clusterE. *) +(* by move=> /(cvg_cluster sFG); exists p. *) +(* Qed. *) +Admitted. -Lemma filter_image (T U : Type) (f : T -> U) (F : set (set T)) : - Filter F -> f @` setT = setT -> Filter [set f @` A | A in F]. +Lemma filter_image (T U : Type) (f : T -> U) (F : {filter T}) : + f @` setT = setT -> is_filter [set f @` A | A in F]. Proof. -move=> FF fsurj; split. -- by exists setT => //; apply: filterT. -- move=> _ _ [A FA <-] [B FB <-]. +set X := [set _ | _ in _]; move=> fsurj; split. +- by exists setT => //; exact: (nearT F). +- move=> P Q [A FA]; rewrite -[[eta P]]/P => <-. + move=> [B FB]; rewrite -[[eta Q]]/Q => <-. exists (f @^-1` (f @` A `&` f @` B)); last by rewrite image_preimage. have sAB : A `&` B `<=` f @^-1` (f @` A `&` f @` B). by move=> x [Ax Bx]; split; exists x. - by apply: filterS sAB _; apply: filterI. + set FAB := f @^-1` _. + rewrite -nbhs_setE. + (* suff: nbhs F FAB by []. *) + (* suff: \for x \near F, FAB x by []. *) + apply: nearS sAB _. apply: nearI. - move=> A B sAB [C FC fC_eqA]. exists (f @^-1` B); last by rewrite image_preimage. - by apply: filterS FC => p Cp; apply: sAB; rewrite -fC_eqA; exists p. -Qed. + suff: nbhs F C -> nbhs F (f @^-1` B) by apply. + by apply: nearS => p Cp; apply: sAB; rewrite -fC_eqA; exists p. +Grab Existential Variables. all: by end_near. Qed. -Lemma proper_image (T U : Type) (f : T -> U) (F : set (set T)) : - ProperFilter F -> f @` setT = setT -> ProperFilter [set f @` A | A in F]. +Lemma proper_image (T U : Type) (f : T -> U) (F : pfilter_on T) : + f @` setT = setT -> is_pfilter [set f @` A | A in F]. Proof. -move=> FF fsurj; apply Build_ProperFilter; last exact: filter_image. -by move=> _ [A FA <-]; have /filter_ex [p Ap] := FA; exists (f p); exists p. -Qed. +move=> fsurj; apply Build_is_pfilter; last exact: filter_image. +move=> _ [A FA <-]. +(* have := (@near_const _ (pfilter_on T) F). *) + +(* have : nbhs (F : {filter T}) A := FA. *) +(* have /near_ex [p Ap] := FA; exists (f p); exists p. *) +(* Qed. *) +Admitted. -Lemma in_ultra_setVsetC T (F : set (set T)) (A : set T) : - UltraFilter F -> F A \/ F (~` A). +Lemma in_ultra_setVsetC T (F : ufilter_on T) (A : set T) : + F A \/ F (~` A). Proof. -move=> FU; case: (pselect (F (~` A))) => [|nFnA]; first by right. -left; suff : ProperFilter (filter_from (F `|` [set A `&` B | B in F]) id). +case: (pselect (F (~` A))) => [|nFnA]; first by right. +left; suff : is_pfilter (nbhs_from (F `|` [set A `&` B | B in F]) id). move=> /max_filter <-; last by move=> B FB; exists B => //; left. - by exists A => //; right; exists setT; [apply: filterT|rewrite setIT]. -apply filter_from_proper; last first. - move=> B [|[C FC <-]]; first exact: filter_ex. + by exists A => //; right; exists setT; [apply: nearT|rewrite setIT]. +apply nbhs_from_proper; last first. + move=> B [|[C FC <-]]; first exact: near_ex. apply: contrapT => /asboolP; rewrite asbool_neg => /forallp_asboolPn AC0. - by apply: nFnA; apply: filterS FC => p Cp Ap; apply: (AC0 p). -apply: filter_from_filter. - by exists A; right; exists setT; [apply: filterT|rewrite setIT]. + by apply: nFnA; apply: nearS FC => p Cp Ap; apply: (AC0 p). +apply: nbhs_from_filter. + by exists A; right; exists setT; [apply: nearT|rewrite setIT]. move=> B C [FB|[DB FDB <-]]. - move=> [FC|[DC FDC <-]]; first by exists (B `&` C)=> //; left; apply: filterI. + move=> [FC|[DC FDC <-]]; first by exists (B `&` C)=> //; left; apply: nearI. exists (A `&` (B `&` DC)); last by rewrite setICA. - by right; exists (B `&` DC) => //; apply: filterI. + by right; exists (B `&` DC) => //; apply: nearI. move=> [FC|[DC FDC <-]]. exists (A `&` (DB `&` C)); last by rewrite setIA. - by right; exists (DB `&` C) => //; apply: filterI. -exists (A `&` (DB `&` DC)); last by move=> ??; rewrite setIACA setIid. -by right; exists (DB `&` DC) => //; apply: filterI. + by right; exists (DB `&` C) => //; apply: nearI. +exists (A `&` (DB `&` DC)); last by move=> ? ?; rewrite setIACA setIid. +by right; exists (DB `&` DC) => //; apply: nearI. Qed. -Lemma ultra_image (T U : Type) (f : T -> U) (F : set (set T)) : - UltraFilter F -> f @` setT = setT -> UltraFilter [set f @` A | A in F]. +Lemma ultra_image (T U : Type) (f : T -> U) (F : {filter T}) : + Ultrais_filter F -> f @` setT = setT -> Ultrais_filter [set f @` A | A in F]. Proof. move=> FU fsurj; split; first exact: proper_image. move=> G GF sfFG; rewrite predeqE => A; split; last exact: sfFG. @@ -2146,7 +2539,7 @@ have [//|FnAf] := in_ultra_setVsetC (f @^-1` A) FU. have : G (f @` (~` (f @^-1` A))) by apply: sfFG; exists (~` (f @^-1` A)). suff : ~ G (f @` (~` (f @^-1` A))) by []. rewrite preimage_setC image_preimage // => GnA. -by have /filter_ex [? []] : G (A `&` (~` A)) by apply: filterI. +by have /near_ex [? []] : G (A `&` (~` A)) by apply: nearI. Qed. Lemma tychonoff (I : eqType) (T : I -> topologicalType) @@ -2168,20 +2561,20 @@ have pr_surj i : @^~ i @` (@setT (forall i, T i)) = setT. rewrite predeqE => pi; split=> // _. by exists (subst_coord i pi (fun _ => point))=> //; rewrite subst_coordT. set pF := fun i => [set @^~ i @` B | B in F]. -have pFultra : forall i, UltraFilter (pF i). +have pFultra : forall i, Ultrais_filter (pF i). by move=> i; apply: ultra_image (pr_surj i). have pFA : forall i, pF i (A i). move=> i; exists [set g | forall i, A i (g i)] => //. rewrite predeqE => pi; split; first by move=> [g Ag <-]; apply: Ag. - move=> Aipi; have [f Af] := filter_ex FA. + move=> Aipi; have [f Af] := near_ex FA. exists (subst_coord i pi f); last exact: subst_coordT. move=> j; case: (eqVneq i j); first by case: _ /; rewrite subst_coordT. by move=> /subst_coordN ->; apply: Af. have cvpFA i : A i `&` [set p | pF i --> p] !=set0. - by rewrite -ultra_flim_clusterE; apply: Aco. + by rewrite -ultra_cvg_clusterE; apply: Aco. exists (fun i => get (A i `&` [set p | pF i --> p])). split=> [i|]; first by have /getPex [] := cvpFA i. -by apply/flim_sup => i; apply/flim_image=> //; have /getPex [] := cvpFA i. +by apply/cvg_sup => i; apply/cvg_image=> //; have /getPex [] := cvpFA i. Qed. End Tychonoff. @@ -2191,9 +2584,9 @@ Definition finI (I : choiceType) T (D : set I) (f : I -> set T) := \bigcap_(i in [set i | i \in D']) f i !=set0. Lemma finI_filter (I : choiceType) T (D : set I) (f : I -> set T) : - finI D f -> ProperFilter (filter_from (finI_from D f) id). + finI D f -> is_pfilter (nbhs_from (finI_from D f) id). Proof. -move=> finIf; apply: (filter_from_proper (filter_from_filter _ _)). +move=> finIf; apply: (nbhs_from_proper (nbhs_from_filter _ _)). - by exists setT; exists fset0 => //; rewrite predeqE. - move=> A B [DA sDA IfA] [DB sDB IfB]; exists (A `&` B) => //. exists (DA `|` DB)%fset. @@ -2201,14 +2594,14 @@ move=> finIf; apply: (filter_from_proper (filter_from_filter _ _)). rewrite -IfA -IfB predeqE => p; split=> [Ifp|[IfAp IfBp] i]. by split=> i Di; apply: Ifp; rewrite in_fsetE Di // orbC. by rewrite in_fsetE => /orP []; [apply: IfAp|apply: IfBp]. -- by move=> _ [?? <-]; apply: finIf. +- by move=> _ [? ? <-]; apply: finIf. Qed. -Lemma filter_finI (T : pointedType) (F : set (set T)) (D : set (set T)) +Lemma filter_finI (T : pointedType) (F : {filter T}) (D : {filter T}) (f : set T -> set T) : - ProperFilter F -> (forall A, D A -> F (f A)) -> finI D f. + is_pfilter F -> (forall A, D A -> F (f A)) -> finI D f. Proof. -move=> FF sDFf D' sD; apply: (@filter_ex _ F); apply: filter_bigI. +move=> FF sDFf D' sD; apply: (@near_ex _ F); apply: filter_bigI. by move=> A /sD; rewrite in_setE => /sDFf. Qed. @@ -2240,7 +2633,7 @@ rewrite predeqE => A; split=> [Aco I D f [g gop feAg] fcov|Aco I D f fop fcov]. exists D' => // p Ap; have /sgcov [i D'i gip] := Ap. by exists i => //; rewrite feAg //; have /sD := D'i; rewrite in_setE. have Afcov : A `<=` \bigcup_(i in D) (A `&` f i). - by move=> p Ap; have /fcov [i ??] := Ap; exists i. + by move=> p Ap; have /fcov [i ? ?] := Ap; exists i. have Afop : open_fam_of A D (fun i => A `&` f i) by exists f. have [D' sD sAfcov] := Aco _ _ _ Afop Afcov. by exists D' => // p /sAfcov [i ? []]; exists i. @@ -2263,16 +2656,16 @@ rewrite predeqE => A; split=> [Aco I D f [g gcl feAg] finIf|Aco F FF FA]. by apply: clfinIfp; exists (f j); [apply: finI_from1|rewrite feAg // => ? []]. have finIAclF : finI F (fun B => A `&` closure B). apply: (@filter_finI _ F) => B FB. - by apply: filterI => //; apply: filterS FB; apply: subset_closure. + by apply: nearI => //; apply: nearS FB; apply: subset_closure. have [|p AclFIp] := Aco _ _ _ _ finIAclF. - by exists closure=> //; move=> ??; apply: closed_closure. + by exists closure=> //; move=> ? ?; apply: closed_closure. exists p; split=> [|B C FB p_C]; first by have /AclFIp [] := FA. by have /AclFIp [_] := FB; move=> /(_ _ p_C). Qed. Lemma exists2P A (P Q : A -> Prop) : (exists2 x, P x & Q x) <-> exists x, P x /\ Q x. -Proof. by split=> [[x ??] | [x []]]; exists x. Qed. +Proof. by split=> [[x ? ?] | [x []]]; exists x. Qed. Lemma compact_cover : compact = cover_compact. Proof. @@ -2330,26 +2723,26 @@ Definition connected (T : topologicalType) (A : set T) := (** * Uniform spaces defined using balls *) -Definition locally_ {T T'} (ball : T -> R -> set T') (x : T) := - @filter_from R _ [set x | 0 < x] (ball x). +Definition nbhs_ {T T'} (ball : T -> R -> set T') (x : T) := + @nbhs_from R _ [set x | 0 < x] (ball x). -Lemma locally_E {T T'} (ball : T -> R -> set T') x : - locally_ ball x = @filter_from R _ [set x : R | 0 < x] (ball x). +Lemma nbhs_E {T T'} (ball : T -> R -> set T') x : + nbhs_ ball x = @nbhs_from R _ [set x : R | 0 < x] (ball x). Proof. by []. Qed. Module Uniform. -Record mixin_of (M : Type) (locally : M -> set (set M)) := Mixin { +Record mixin_of (M : Type) (nbhs : M -> {filter M}) := Mixin { ball : M -> R -> M -> Prop ; ax1 : forall x (e : R), 0 < e -> ball x e x ; ax2 : forall x y (e : R), ball x e y -> ball y e x ; ax3 : forall x y z e1 e2, ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z; - ax4 : locally = locally_ ball + ax4 : nbhs = nbhs_ ball }. Record class_of (M : Type) := Class { base : Topological.class_of M; - mixin : mixin_of (Filtered.locally_op base) + mixin : mixin_of (Filter.nbhs_op base) }. Section ClassDef. @@ -2367,13 +2760,13 @@ Local Coercion mixin : class_of >-> mixin_of. Definition pack loc (m : @mixin_of T loc) := fun bT (b : Topological.class_of T) of phant_id (@Topological.class bT) b => - fun m' of phant_id m (m' : @mixin_of T (Filtered.locally_op b)) => + fun m' of phant_id m (m' : @mixin_of T (Filter.nbhs_op b)) => @Pack T (@Class _ b m') T. Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. Definition pointedType := @Pointed.Pack cT xclass xT. -Definition filteredType := @Filtered.Pack cT cT xclass xT. +Definition filterType := @Filter.Pack cT cT xclass xT. Definition topologicalType := @Topological.Pack cT xclass xT. End ClassDef. @@ -2389,8 +2782,8 @@ Coercion choiceType : type >-> Choice.type. Canonical choiceType. Coercion pointedType : type >-> Pointed.type. Canonical pointedType. -Coercion filteredType : type >-> Filtered.type. -Canonical filteredType. +Coercion filterType : type >-> Filter.type. +Canonical filterType. Coercion topologicalType : type >-> Topological.type. Canonical topologicalType. Notation uniformType := type. @@ -2409,7 +2802,7 @@ Export Uniform.Exports. Section UniformTopology. -Lemma my_ball_le (M : Type) (loc : M -> set (set M)) +Lemma my_ball_le (M : Type) (loc : M -> {filter M}) (m : Uniform.mixin_of loc) : forall (x : M) (e1 e2 : R), e1 <= e2 -> forall (y : M), Uniform.ball m x e1 y -> Uniform.ball m x e2 y. @@ -2422,27 +2815,27 @@ suff : Uniform.ball m x (PosNum lt12)%:num x by []. exact: Uniform.ax1. Qed. -Program Definition topologyOfBallMixin (T : Type) - (loc : T -> set (set T)) (m : Uniform.mixin_of loc) : - Topological.mixin_of loc := topologyOfFilterMixin _ _ _. +Program Definition OfBall.topologyMixin (T : Type) + (loc : T -> {filter T}) (m : Uniform.mixin_of loc) : + Topological.mixin_of loc := OfFilter.topologyMixin _ _ _. Next Obligation. -rewrite (Uniform.ax4 m) locally_E; apply filter_from_proper; last first. +rewrite (Uniform.ax4 m) nbhs_E; apply nbhs_from_proper; last first. move=> e egt0; exists p; suff : Uniform.ball m p (PosNum egt0)%:num p by []. exact: Uniform.ax1. -apply: filter_from_filter; first by exists 1%:pos%:num. +apply: nbhs_from_filter; first by exists 1%:pos%:num. move=> e1 e2 e1gt0 e2gt0; exists (Num.min e1 e2). by have := min_pos_gt0 (PosNum e1gt0) (PosNum e2gt0). by move=> q pmin_q; split; apply: my_ball_le pmin_q; rewrite ler_minl lerr // orbC. Qed. Next Obligation. -move: H; rewrite (Uniform.ax4 m) locally_E => - [e egt0]; apply. +move: H; rewrite (Uniform.ax4 m) nbhs_E => - [e egt0]; apply. by have : Uniform.ball m p (PosNum egt0)%:num p by exact: Uniform.ax1. Qed. Next Obligation. -move: H; rewrite (Uniform.ax4 m) locally_E => - [e egt0 pe_A]. +move: H; rewrite (Uniform.ax4 m) nbhs_E => - [e egt0 pe_A]. exists ((PosNum egt0)%:num / 2) => // q phe_q. -rewrite locally_E; exists ((PosNum egt0)%:num / 2) => // r qhe_r. +rewrite nbhs_E; exists ((PosNum egt0)%:num / 2) => // r qhe_r. by apply: pe_A; rewrite [e]splitr; apply: Uniform.ax3 qhe_r. Qed. @@ -2450,20 +2843,20 @@ End UniformTopology. Definition ball {M : uniformType} := Uniform.ball (Uniform.class M). -Lemma locally_ballE {M : uniformType} : locally_ (@ball M) = locally. +Lemma nbhs_ballE {M : uniformType} : nbhs_ (@ball M) = nbhs. Proof. by case: M=> [?[?[]]]. Qed. -Lemma filter_from_ballE {M : uniformType} x : - @filter_from R _ [set x : R | 0 < x] (@ball M x) = locally x. -Proof. by rewrite -locally_ballE. Qed. +Lemma nbhs_from_ballE {M : uniformType} x : + @nbhs_from R _ [set x : R | 0 < x] (@ball M x) = nbhs x. +Proof. by rewrite -nbhs_ballE. Qed. -Module Export LocallyBall. -Definition locally_simpl := (locally_simpl,@filter_from_ballE,@locally_ballE). -End LocallyBall. +Module Export NbhsBall. +Definition nbhs_simpl := (nbhs_simpl,@nbhs_from_ballE,@nbhs_ballE). +End NbhsBall. -Lemma locallyP {M : uniformType} (x : M) P : - locally x P <-> locally_ ball x P. -Proof. by rewrite locally_simpl. Qed. +Lemma nbhsP {M : uniformType} (x : M) P : + nbhs x P <-> nbhs_ ball x P. +Proof. by rewrite nbhs_simpl. Qed. Section uniformType1. Context {M : uniformType}. @@ -2503,134 +2896,134 @@ Qed. Lemma ball_le (x : M) (e1 e2 : R) : (e1 <= e2)%coqR -> ball x e1 `<=` ball x e2. Proof. by move=> /RleP/ball_ler. Qed. -Lemma locally_ball (x : M) (eps : posreal) : locally x (ball x eps%:num). -Proof. by apply/locallyP; exists eps%:num. Qed. -Hint Resolve locally_ball : core. +Lemma nbhs_ball (x : M) (eps : posreal) : nbhs x (ball x eps%:num). +Proof. by apply/nbhsP; exists eps%:num. Qed. +Hint Resolve nbhs_ball : core. Definition close (x y : M) : Prop := forall eps : posreal, ball x eps%:num y. Lemma close_refl (x : M) : close x x. Proof. by []. Qed. Lemma close_sym (x y : M) : close x y -> close y x. -Proof. by move=> ??; apply: ball_sym. Qed. +Proof. by move=> ? ?; apply: ball_sym. Qed. Lemma close_trans (x y z : M) : close x y -> close y z -> close x z. Proof. by move=> cxy cyz eps; apply: ball_split (cxy _) (cyz _). Qed. Lemma close_limxx (x y : M) : close x y -> x --> y. Proof. -move=> cxy P /= /locallyP /= [_/posnumP [eps] epsP]. -apply/locallyP; exists (eps%:num / 2) => // z bxz. +move=> cxy P /= /nbhsP /= [_/posnumP [eps] epsP]. +apply/nbhsP; exists (eps%:num / 2) => // z bxz. by apply: epsP; apply: ball_splitr (cxy _) bxz. Qed. Definition entourages : set (set (M * M)):= - filter_from [set eps : R | eps > 0] + nbhs_from [set eps : R | eps > 0] (fun eps => [set xy | ball xy.1 eps xy.2]). -Global Instance entourages_filter : ProperFilter entourages. +Global Instance entourages_filter : is_pfilter entourages. Proof. -apply filter_from_proper; last by exists (point,point); apply: ballxx. -apply: filter_from_filter; first by exists 1; rewrite ltr01. +apply nbhs_from_proper; last by exists (point,point); apply: ballxx. +apply: nbhs_from_filter; first by exists 1; rewrite ltr01. move=> _ _ /posnumP[i] /posnumP[j]; exists (minr i j) => // [[/= x y]] bxy. by eexists => /=; apply: ball_ler bxy; rewrite ler_minl lerr ?orbT. Qed. Typeclasses Opaque entourages. -Lemma flim_close {F} {FF : ProperFilter F} (x y : M) : +Lemma cvg_close {F} {FF : is_pfilter F} (x y : M) : F --> x -> F --> y -> close x y. Proof. move=> Fx Fy e; near F => z; apply: (@ball_splitl z); near: z; -by [apply/Fx/locally_ball|apply/Fy/locally_ball]. +by [apply/Fx/nbhs_ball|apply/Fy/nbhs_ball]. Grab Existential Variables. all: end_near. Qed. -Lemma flimx_close (x y : M) : x --> y -> close x y. -Proof. exact: flim_close. Qed. +Lemma cvgx_close (x y : M) : x --> y -> close x y. +Proof. exact: cvg_close. Qed. Lemma near_ball (y : M) (eps : posreal) : - \forall y' \near y, ball y eps%:num y'. -Proof. exact: locally_ball. Qed. + \for y' \near y, ball y eps%:num y'. +Proof. exact: nbhs_ball. Qed. -Lemma flim_ballP {F} {FF : Filter F} (y : M) : - F --> y <-> forall eps : R, 0 < eps -> \forall y' \near F, ball y eps y'. -Proof. by rewrite -filter_fromP !locally_simpl /=. Qed. -Definition flim_locally := @flim_ballP. +Lemma cvg_ballP {F} {FF : is_filter F} (y : M) : + F --> y <-> forall eps : R, 0 < eps -> \for y' \near F, ball y eps y'. +Proof. by rewrite -nbhs_fromP !nbhs_simpl /=. Qed. +Definition cvg_nbhs := @cvg_ballP. -Lemma flim_ballPpos {F} {FF : Filter F} (y : M) : - F --> y <-> forall eps : {posnum R}, \forall y' \near F, ball y eps%:num y'. +Lemma cvg_ballPpos {F} {FF : is_filter F} (y : M) : + F --> y <-> forall eps : {posnum R}, \for y' \near F, ball y eps%:num y'. Proof. -by split => [/flim_ballP|] pos; [case|apply/flim_ballP=> _/posnumP[eps] //]. +by split => [/cvg_ballP|] pos; [case|apply/cvg_ballP=> _/posnumP[eps] //]. Qed. -Lemma flim_ball {F} {FF : Filter F} (y : M) : - F --> y -> forall eps : R, 0 < eps -> \forall y' \near F, ball y eps y'. -Proof. by move/flim_ballP. Qed. +Lemma cvg_ball {F} {FF : is_filter F} (y : M) : + F --> y -> forall eps : R, 0 < eps -> \for y' \near F, ball y eps y'. +Proof. by move/cvg_ballP. Qed. -Lemma app_flim_locally T {F} {FF : Filter F} (f : T -> M) y : - f @ F --> y <-> forall eps : R, 0 < eps -> \forall x \near F, ball y eps (f x). -Proof. exact: flim_ballP. Qed. +Lemma app_cvg_nbhs T {F} {FF : is_filter F} (f : T -> M) y : + f @ F --> y <-> forall eps : R, 0 < eps -> \for x \near F, ball y eps (f x). +Proof. exact: cvg_ballP. Qed. -Lemma flimi_ballP T {F} {FF : Filter F} (f : T -> M -> Prop) y : +Lemma cvgi_ballP T {F} {FF : is_filter F} (f : T -> M -> Prop) y : f `@ F --> y <-> - forall eps : R, 0 < eps -> \forall x \near F, exists z, f x z /\ ball y eps z. + forall eps : R, 0 < eps -> \for x \near F, exists z, f x z /\ ball y eps z. Proof. -split=> [Fy _/posnumP[eps] |Fy P] /=; first exact/Fy/locally_ball. -move=> /locallyP[_ /posnumP[eps] subP]. +split=> [Fy _/posnumP[eps] |Fy P] /=; first exact/Fy/nbhs_ball. +move=> /nbhsP[_ /posnumP[eps] subP]. rewrite near_simpl near_mapi; near=> x. have [//|z [fxz yz]] := near (Fy _ (posnum_gt0 eps)) x. by exists z => //; split => //; apply: subP. Unshelve. all: end_near. Qed. -Definition flimi_locally := @flimi_ballP. +Definition cvgi_nbhs := @cvgi_ballP. -Lemma flimi_ball T {F} {FF : Filter F} (f : T -> M -> Prop) y : +Lemma cvgi_ball T {F} {FF : is_filter F} (f : T -> M -> Prop) y : f `@ F --> y -> forall eps : R, 0 < eps -> F [set x | exists z, f x z /\ ball y eps z]. -Proof. by move/flimi_ballP. Qed. +Proof. by move/cvgi_ballP. Qed. -Lemma flimi_close T {F} {FF: ProperFilter F} (f : T -> set M) (l l' : M) : +Lemma cvgi_close T {F} {FF: is_pfilter F} (f : T -> set M) (l l' : M) : {near F, is_fun f} -> f `@ F --> l -> f `@ F --> l' -> close l l'. Proof. move=> f_prop fFl fFl'. -suff f_totalfun: infer {near F, is_totalfun f} by exact: flim_close fFl fFl'. +suff f_totalfun: infer {near F, is_totalfun f} by exact: cvg_close fFl fFl'. apply: filter_app f_prop; near=> x; split=> //=. -by have [//|y [fxy _]] := near (flimi_ball fFl [gt0 of 1]) x; exists y. +by have [//|y [fxy _]] := near (cvgi_ball fFl [gt0 of 1]) x; exists y. Grab Existential Variables. all: end_near. Qed. -Definition flimi_locally_close := @flimi_close. +Definition cvgi_nbhs_close := @cvgi_close. -Lemma flim_const {T} {F : set (set T)} - {FF : Filter F} (a : M) : a @[_ --> F] --> a. +Lemma cvg_const {T} {F : {filter T}} + {FF : is_filter F} (a : M) : a @[_ --> F] --> a. Proof. -move=> P /locallyP[_ /posnumP[eps] subP]; rewrite !near_simpl /=. +move=> P /nbhsP[_ /posnumP[eps] subP]; rewrite !near_simpl /=. by apply: filterE=> ?; apply/subP. Qed. -Lemma close_lim (F1 F2 : set (set M)) {FF2 : ProperFilter F2} : +Lemma close_lim (F1 F2 : {filter M}) {FF2 : is_pfilter F2} : F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2). Proof. -move=> F12 F21; have [/(flim_trans F21) F2l|dvgF1] := pselect (cvg F1). - by apply: (@flim_close F2) => //; apply: cvgP F2l. -have [/(flim_trans F12)/cvgP//|dvgF2] := pselect (cvg F2). +move=> F12 F21; have [/(cvg_trans F21) F2l|dvgF1] := pselect (cvg F1). + by apply: (@cvg_close F2) => //; apply: cvgP F2l. +have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2). by rewrite dvgP // dvgP //. Qed. -Lemma flim_closeP (F : set (set M)) (l : M) : ProperFilter F -> +Lemma cvg_closeP (F : {filter M}) (l : M) : is_pfilter F -> F --> l <-> ([cvg F in M] /\ close (lim F) l). Proof. move=> FF; split=> [Fl|[cvF]Cl]. - by have /cvgP := Fl; split=> //; apply: (@flim_close F). -by apply: flim_trans (close_limxx Cl). + by have /cvgP := Fl; split=> //; apply: (@cvg_close F). +by apply: cvg_trans (close_limxx Cl). Qed. Definition ball_set (A : set M) e := \bigcup_(p in A) ball p e. -Canonical set_filter_source := - @Filtered.Source Prop _ M (fun A => locally_ ball_set A). +Canonical set_filter_source := Eval hnf in + @Filter.Source Prop _ M (fun A => nbhs_ ball_set A). End uniformType1. Hint Resolve ball_center : core. Hint Resolve close_refl : core. -Hint Resolve locally_ball : core. -Arguments flim_const {M T F FF} a. +Hint Resolve nbhs_ball : core. +Arguments cvg_const {M T F FF} a. Arguments close_lim {M} F1 F2 {FF2} _. Section entourages. @@ -2642,7 +3035,7 @@ Lemma unif_contP (U V : uniformType) (f : U -> V) : unif_cont f <-> forall e, e > 0 -> exists2 d, d > 0 & forall x, ball x.1 d x.2 -> ball (f x.1) e (f x.2). -Proof. exact: filter_fromP. Qed. +Proof. exact: nbhs_fromP. Qed. End entourages. @@ -2659,15 +3052,15 @@ Implicit Types x y : 'M[T]_(m, n). Definition mx_ball x (e : R) y := forall i j, ball (x i j) e (y i j). Lemma mx_ball_center x (e : R) : 0 < e -> mx_ball x e x. -Proof. by move=> ???; apply: ballxx. Qed. +Proof. by move=> ? ? ?; apply: ballxx. Qed. Lemma mx_ball_sym x y (e : R) : mx_ball x e y -> mx_ball y e x. -Proof. by move=> xe_y ??; apply/ball_sym/xe_y. Qed. +Proof. by move=> xe_y ? ?; apply/ball_sym/xe_y. Qed. Lemma mx_ball_triangle x y z (e1 e2 : R) : mx_ball x e1 y -> mx_ball y e2 z -> mx_ball x (e1 + e2) z. Proof. -by move=> xe1_y ye2_z ??; apply: ball_triangle; [apply: xe1_y| apply: ye2_z]. +by move=> xe1_y ye2_z ? ?; apply: ball_triangle; [apply: xe1_y| apply: ye2_z]. Qed. Lemma ltr_bigminr (I : finType) (R : realDomainType) (f : I -> R) (x0 x : R) : @@ -2685,13 +3078,13 @@ by rewrite inE => /orP [/eqP->|/ihl leminlfi]; rewrite ler_minl ?lerr // leminlfi orbC. Qed. -Canonical R_pointedType := PointedType R 0. +Canonical R_pointedType := Eval hnf in PointedType R 0. -Lemma mx_locally : locally = locally_ mx_ball. +Lemma mx_nbhs : nbhs = nbhs_ mx_ball. Proof. rewrite predeq2E => x A; split; last first. by move=> [e egt0 xe_A]; exists (fun i j => ball (x i j) (PosNum egt0)%:num). -move=> [P]; rewrite -locally_ballE => x_P sPA. +move=> [P]; rewrite -nbhs_ballE => x_P sPA. exists (\big[minr/1]_i \big[minr/1]_j get (fun e : R => 0 < e /\ ball (x i j) e `<=` P i j)). apply: ltr_bigminr => // i; apply: ltr_bigminr => // j. @@ -2701,10 +3094,10 @@ apply: ball_ler (xmin_y i j). by apply: ler_trans (bigminr_ler _ _ i) _; apply: bigminr_ler. Qed. -Definition matrix_uniformType_mixin := - Uniform.Mixin mx_ball_center mx_ball_sym mx_ball_triangle mx_locally. +Definition matrix_uniformType_mixin := Eval hnf in + Uniform.Mixin mx_ball_center mx_ball_sym mx_ball_triangle mx_nbhs. -Canonical matrix_uniformType := +Canonical matrix_uniformType := Eval hnf in UniformType 'M[T]_(m, n) matrix_uniformType_mixin. End matrix_Uniform. @@ -2733,11 +3126,11 @@ Proof. by move=> [bxy1 bxy2] [byz1 byz2]; split; eapply ball_triangle; eassumption. Qed. -Lemma prod_locally : locally = locally_ prod_ball. +Lemma prod_nbhs : nbhs = nbhs_ prod_ball. Proof. rewrite predeq2E => -[x y] P; split=> [[[A B] /=[xX yY] XYP] |]; last first. by move=> [_ /posnumP[eps] epsP]; exists (ball x eps%:num, ball y eps%:num) => /=. -move: xX yY => /locallyP [_ /posnumP[ex] eX] /locallyP [_ /posnumP[ey] eY]. +move: xX yY => /nbhsP [_ /posnumP[ex] eX] /nbhsP [_ /posnumP[ey] eY]. exists (minr ex%:num ey%:num) => // -[x' y'] [/= xx' yy']. apply: XYP; split=> /=. by apply/eX/(ball_ler _ xx'); rewrite ler_minl lerr. @@ -2745,25 +3138,25 @@ by apply/eY/(ball_ler _ yy'); rewrite ler_minl lerr orbT. Qed. Definition prod_uniformType_mixin := - Uniform.Mixin prod_ball_center prod_ball_sym prod_ball_triangle prod_locally. + Uniform.Mixin prod_ball_center prod_ball_sym prod_ball_triangle prod_nbhs. End prod_Uniform. -Canonical prod_uniformType (U V : uniformType) := +Canonical prod_uniformType (U V : uniformType) := Eval hnf in UniformType (U * V) (@prod_uniformType_mixin U V). -Section Locally_fct2. +Section Nbhs_fct2. Context {T : Type} {U V : uniformType}. -Lemma flim_ball2P {F : set (set U)} {G : set (set V)} - {FF : Filter F} {FG : Filter G} (y : U) (z : V): +Lemma cvg_ball2P {F : {filter U}} {G : {filter V}} + {FF : is_filter F} {FG : is_filter G} (y : U) (z : V): (F, G) --> (y, z) <-> - forall eps : R, eps > 0 -> \forall y' \near F & z' \near G, + forall eps : R, eps > 0 -> \for y' \near F & z' \near G, ball y eps y' /\ ball z eps z'. -Proof. exact: flim_ballP. Qed. +Proof. exact: cvg_ballP. Qed. -End Locally_fct2. +End Nbhs_fct2. (** Functional metric spaces *) @@ -2788,27 +3181,27 @@ Definition fct_uniformType_mixin := UniformMixin fct_ball_center fct_ball_sym fct_ball_triangle erefl. Definition fct_topologicalTypeMixin := - topologyOfBallMixin fct_uniformType_mixin. + OfBall.topologyMixin fct_uniformType_mixin. -Canonical generic_source_filter := @Filtered.Source _ _ _ (locally_ fct_ball). -Canonical fct_topologicalType := +Canonical generic_source_filter := Eval hnf in @Filter.Source _ _ _ (nbhs_ fct_ball). +Canonical fct_topologicalType := Eval hnf in TopologicalType (T -> U) fct_topologicalTypeMixin. -Canonical fct_uniformType := UniformType (T -> U) fct_uniformType_mixin. +Canonical fct_uniformType := Eval hnf in UniformType (T -> U) fct_uniformType_mixin. End fct_Uniform. (** ** Complete uniform spaces *) (* :TODO: Use cauchy2 alternative to define cauchy? *) -(* Or not: is the fact that cauchy F -/> ProperFilter F a problem? *) -Definition cauchy_ex {T : uniformType} (F : set (set T)) := +(* Or not: is the fact that cauchy F -/> is_pfilter F a problem? *) +Definition cauchy_ex {T : uniformType} (F : {filter T}) := forall eps : R, 0 < eps -> exists x, F (ball x eps). -Definition cauchy {T : uniformType} (F : set (set T)) := - forall e, e > 0 -> \forall x & y \near F, ball x e y. +Definition cauchy {T : uniformType} (F : {filter T}) := + forall e, e > 0 -> \for x & y \near F, ball x e y. -Lemma cauchy_entouragesP (T : uniformType) (F : set (set T)) : - Filter F -> cauchy F <-> (F, F) --> entourages. +Lemma cauchy_entouragesP (T : uniformType) (F : {filter T}) : + is_filter F -> cauchy F <-> (F, F) --> entourages. Proof. move=> FF; split=> cauchyF; last first. by move=> _/posnumP[eps]; apply: cauchyF; exists eps%:num. @@ -2816,11 +3209,11 @@ move=> U [_/posnumP[eps] xyepsU]. by near=> x; apply: xyepsU; near: x; apply: cauchyF. Grab Existential Variables. all: end_near. Qed. -Lemma cvg_cauchy_ex {T : uniformType} (F : set (set T)) : +Lemma cvg_cauchy_ex {T : uniformType} (F : {filter T}) : [cvg F in T] -> cauchy_ex F. -Proof. by move=> Fl _/posnumP[eps]; exists (lim F); apply/Fl/locally_ball. Qed. +Proof. by move=> Fl _/posnumP[eps]; exists (lim F); apply/Fl/nbhs_ball. Qed. -Lemma cauchy_exP (T : uniformType) (F : set (set T)) : Filter F -> +Lemma cauchy_exP (T : uniformType) (F : {filter T}) : is_filter F -> cauchy_ex F -> cauchy F. Proof. move=> FF Fc; apply/cauchy_entouragesP => A [_/posnumP[e] sdeA]. @@ -2828,21 +3221,21 @@ have /Fc [z /= Fze] := [gt0 of e%:num / 2]; near=> x y; apply: sdeA => /=. by apply: (@ball_splitr _ z); [near: x|near: y]. Grab Existential Variables. all: end_near. Qed. -Lemma cauchyP (T : uniformType) (F : set (set T)) : ProperFilter F -> +Lemma cauchyP (T : uniformType) (F : {filter T}) : is_pfilter F -> cauchy F <-> cauchy_ex F. Proof. move=> FF; split=> [Fcauchy _/posnumP[e] |/cauchy_exP//]. by near F => x; exists x; near: x; apply: (@nearP_dep _ _ F F); apply: Fcauchy. Grab Existential Variables. all: end_near. Qed. -Lemma cvg_cauchy {T : uniformType} (F : set (set T)) : Filter F -> +Lemma cvg_cauchy {T : uniformType} (F : {filter T}) : is_filter F -> [cvg F in T] -> cauchy F. Proof. by move=> FF /cvg_cauchy_ex /cauchy_exP. Qed. Module Complete. Definition axiom (T : uniformType) := - forall (F : set (set T)), ProperFilter F -> cauchy F -> F --> lim F. + forall (F : {filter T}), is_pfilter F -> cauchy F -> F --> lim F. Section ClassDef. @@ -2871,7 +3264,7 @@ Definition pack b0 (m0 : axiom (@Uniform.Pack T b0 T)) := Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. Definition pointedType := @Pointed.Pack cT xclass xT. -Definition filteredType := @Filtered.Pack cT cT xclass xT. +Definition filterType := @Filter.Pack cT cT xclass xT. Definition topologicalType := @Topological.Pack cT xclass xT. Definition uniformType := @Uniform.Pack cT xclass xT. @@ -2888,8 +3281,8 @@ Coercion choiceType : type >-> Choice.type. Canonical choiceType. Coercion pointedType : type >-> Pointed.type. Canonical pointedType. -Coercion filteredType : type >-> Filtered.type. -Canonical filteredType. +Coercion filterType : type >-> Filter.type. +Canonical filterType. Coercion topologicalType : type >-> Topological.type. Canonical topologicalType. Coercion uniformType : type >-> Uniform.type. @@ -2911,7 +3304,7 @@ Section completeType1. Context {T : completeType}. -Lemma complete_cauchy (F : set (set T)) (FF : ProperFilter F) : +Lemma complete_cauchy (F : {filter T}) (FF : is_pfilter F) : cauchy F -> F --> lim F. Proof. by case: T F FF => [? [?]]. Qed. @@ -2923,21 +3316,21 @@ Section matrix_Complete. Variables (T : completeType) (m n : nat). Lemma mx_complete (F : set (set 'M[T]_(m, n))) : - ProperFilter F -> cauchy F -> cvg F. + is_pfilter F -> cauchy F -> cvg F. Proof. move=> FF Fc. have /(_ _ _) /complete_cauchy cvF : cauchy ((fun M : 'M[T]_(m, n) => M _ _) @ F). - by move=> ?? _ /posnumP[e]; rewrite near_simpl; apply: filterS (Fc _ _). + by move=> ? ? _ /posnumP[e]; rewrite near_simpl; apply: nearS (Fc _ _). apply/cvg_ex. exists (\matrix_(i, j) (lim ((fun M : 'M[T]_(m, n) => M i j) @ F) : T)). -apply/flim_ballP => _ /posnumP[e]; near=> M => i j. +apply/cvg_ballP => _ /posnumP[e]; near=> M => i j. rewrite mxE; near F => M' => /=; apply: (@ball_splitl _ (M' i j)). - by near: M'; apply/cvF/locally_ball. -by move: (i) (j); near: M'; near: M; apply: nearP_dep; apply: filterS (Fc _ _). + by near: M'; apply/cvF/nbhs_ball. +by move: (i) (j); near: M'; near: M; apply: nearP_dep; apply: nearS (Fc _ _). Grab Existential Variables. all: end_near. Qed. -Canonical matrix_completeType := CompleteType 'M[T]_(m, n) mx_complete. +Canonical matrix_completeType := Eval hnf in CompleteType 'M[T]_(m, n) mx_complete. End matrix_Complete. @@ -2946,67 +3339,67 @@ Section fun_Complete. Context {T : choiceType} {U : completeType}. Lemma fun_complete (F : set (set (T -> U))) - {FF : ProperFilter F} : cauchy F -> cvg F. + {FF : is_pfilter F} : cauchy F -> cvg F. Proof. move=> Fc; have /(_ _) /complete_cauchy Ft_cvg : cauchy (@^~_ @ F). - by move=> t e ?; rewrite near_simpl; apply: filterS (Fc _ _). + by move=> t e ?; rewrite near_simpl; apply: nearS (Fc _ _). apply/cvg_ex; exists (fun t => lim (@^~t @ F)). -apply/flim_ballPpos => e; near=> f => t; near F => g => /=. -apply: (@ball_splitl _ (g t)); first by near: g; exact/Ft_cvg/locally_ball. -by move: (t); near: g; near: f; apply: nearP_dep; apply: filterS (Fc _ _). +apply/cvg_ballPpos => e; near=> f => t; near F => g => /=. +apply: (@ball_splitl _ (g t)); first by near: g; exact/Ft_cvg/nbhs_ball. +by move: (t); near: g; near: f; apply: nearP_dep; apply: nearS (Fc _ _). Grab Existential Variables. all: end_near. Qed. -Canonical fun_completeType := CompleteType (T -> U) fun_complete. +Canonical fun_completeType := Eval hnf in CompleteType (T -> U) fun_complete. End fun_Complete. (** ** Limit switching *) -Section Flim_switch. +Section Cvg_switch. Context {T1 T2 : choiceType}. -Lemma flim_switch_1 {U : uniformType} - F1 {FF1 : ProperFilter F1} F2 {FF2 : Filter F2} +Lemma cvg_switch_1 {U : uniformType} + F1 {FF1 : is_pfilter F1} F2 {FF2 : is_filter F2} (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) (l : U) : f @ F1 --> g -> (forall x1, f x1 @ F2 --> h x1) -> h @ F1 --> l -> g @ F2 --> l. Proof. -move=> fg fh hl; apply/flim_ballPpos => e. +move=> fg fh hl; apply/cvg_ballPpos => e. rewrite near_simpl; near F1 => x1; near=> x2. -apply: (@ball_split _ (h x1)); first by near: x1; apply/hl/locally_ball. -apply: (@ball_splitl _ (f x1 x2)); first by near: x2; apply/fh/locally_ball. -by move: (x2); near: x1; apply/(flim_ball fg). +apply: (@ball_split _ (h x1)); first by near: x1; apply/hl/nbhs_ball. +apply: (@ball_splitl _ (f x1 x2)); first by near: x2; apply/fh/nbhs_ball. +by move: (x2); near: x1; apply/(cvg_ball fg). Grab Existential Variables. all: end_near. Qed. -Lemma flim_switch_2 {U : completeType} - F1 {FF1 : ProperFilter F1} F2 {FF2 : ProperFilter F2} +Lemma cvg_switch_2 {U : completeType} + F1 {FF1 : is_pfilter F1} F2 {FF2 : is_pfilter F2} (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) : f @ F1 --> g -> (forall x, f x @ F2 --> h x) -> [cvg h @ F1 in U]. Proof. move=> fg fh; apply: complete_cauchy => _/posnumP[e]. rewrite !near_simpl; near=> x1 y1=> /=; near F2 => x2. -apply: (@ball_splitl _ (f x1 x2)); first by near: x2; apply/fh/locally_ball. -apply: (@ball_split _ (f y1 x2)); first by near: x2; apply/fh/locally_ball. +apply: (@ball_splitl _ (f x1 x2)); first by near: x2; apply/fh/nbhs_ball. +apply: (@ball_split _ (f y1 x2)); first by near: x2; apply/fh/nbhs_ball. apply: (@ball_splitr _ (g x2)); move: (x2); [near: y1|near: x1]; -by apply/(flim_ball fg). +by apply/(cvg_ball fg). Grab Existential Variables. all: end_near. Qed. (* Alternative version *) -(* Lemma flim_switch {U : completeType} *) -(* F1 (FF1 : ProperFilter F1) F2 (FF2 : ProperFilter F2) (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) : *) +(* Lemma cvg_switch {U : completeType} *) +(* F1 (FF1 : is_pfilter F1) F2 (FF2 : is_pfilter F2) (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) : *) (* [cvg f @ F1 in T2 -> U] -> (forall x, [cvg f x @ F2 in U]) -> *) (* [/\ [cvg [lim f @ F1] @ F2 in U], [cvg (fun x => [lim f x @ F2]) @ F1 in U] *) (* & [lim [lim f @ F1] @ F2] = [lim (fun x => [lim f x @ F2]) @ F1]]. *) -Lemma flim_switch {U : completeType} - F1 (FF1 : ProperFilter F1) F2 (FF2 : ProperFilter F2) +Lemma cvg_switch {U : completeType} + F1 (FF1 : is_pfilter F1) F2 (FF2 : is_pfilter F2) (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) : f @ F1 --> g -> (forall x1, f x1 @ F2 --> h x1) -> exists l : U, h @ F1 --> l /\ g @ F2 --> l. Proof. -move=> Hfg Hfh; have hcv := !! flim_switch_2 Hfg Hfh. -by exists [lim h @ F1 in U]; split=> //; apply: flim_switch_1 Hfg Hfh hcv. +move=> Hfg Hfh; have hcv := !! cvg_switch_2 Hfg Hfh. +by exists [lim h @ F1 in U]; split=> //; apply: cvg_switch_1 Hfg Hfh hcv. Qed. -End Flim_switch. +End Cvg_switch.