Module mathcomp.classical.filter

From HB Require Import structures.
From mathcomp Require Import boot order algebra finmap.
From mathcomp Require Import boolp classical_sets functions wochoice
cardinality fsbigop set_interval.

# Filters The theory of (powerset) filters and tools for manipulating them. This file introduces convergence for filters. It also provides the interface of filtered types for associating a "canonical filter" to each element. And lastly it provides typeclass instances for verifying when a (set_system T) is really a filter in T, as a Filter or Properfilter. ## Structure of filter ``` filteredType 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. The HB class is called Filtered. It extends Pointed. nbhs p == set of sets associated to p (in a filtered type) pfilteredType U == a pointed and filtered type hasNbhs == factory for filteredType nbhsType == type of a structure that has a set system of neighborhoods associated to each point pnbhsType == same has nbhsType for pointed types continuous f == f is continuous w.r.t the topology isSubNbhs V S U == interface that states the continuity of val for U which has a subChoiceType and a nbhsType subNbhsType V S == structure that extends a subChoiceType/nbhsType with the isSubNbhs interface The HB class is SubNbhs. filterI_iter F n == nth stage of recursively building the filter of finite intersections of F open_finI_from D f == set of \bigcap_(i in E) f i where E is a a finite subset of D ``` We endow several standard types with the structure of filter, e.g.: - products `(X1 * X2)%type` - matrices `'M[X]_(m, n)` - natural numbers `nat` ## Theory of filters ``` filter_from D B == set of the supersets of the elements of the family of sets B whose indices are in the domain D This is a filter if (B_i)_(i in D) forms a filter base. filter_prod F G == product of the filters F and G F `=>` G <-> G is included in F F and G are sets of sets. \oo == "eventually" filter on nat: set of predicates on natural numbers that are eventually true F --> G <-> the canonical filter associated to G is included in the canonical filter associated to F lim F == limit of the canonical filter associated with F if there is such a limit, i.e., an element l such that the canonical filter associated to l is a subset of F [lim F in T] == limit of the canonical filter associated to F in T where T has type filteredType U [cvg F in T] <-> the canonical filter associated to F converges in T 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 sets F is a filter ProperFilter 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 filter_on T == interface type for sets of sets on T that are filters FilterType F FF == packs the set of sets F with the proof FF of Filter F to build a filter_on T structure 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 pfilter_on T structure fmap f F == image of the filter F by the function f E @[x --> F] == image of the canonical filter associated to F by the function (fun x => E) f @ F == image of the canonical filter associated to F by the function f fmapi f F == image of the filter F by the relation f E `@[x --> F] == image of the canonical filter associated to F by the relation (fun x => E) f `@ F == image of the canonical filter associated to F by the relation f globally A == filter of the sets containing A @frechet_filter T := [set S : set T | finite_set (~` S)] a.k.a. cofinite filter within D F == restriction of the filter F to the domain D principal_filter x == filter containing every superset of x principal_filter_type == alias for choice types with principal filters subset_filter F D == similar to within D F, but with dependent types powerset_filter_from F == the filter of downward closed subsets of F. Enables use of near notation to pick suitably small members of F in_filter F == interface type for the sets that belong to the set of sets F InFilter FP == packs a set P with a proof of F P to build a in_filter F structure ``` ## Near notations and tactics The purpose of the near notations and tactics is to make the manipulation of filters easier. Instead of proving $F\; G$, one can prove $G\; x$ for $x$ "near F", i.e., for x such that H x for H arbitrarily precise as long as $F\; H$. The near tactics allow for a delayed introduction of $H$: $H$ is introduced as an existential variable and progressively instantiated during the proof process. ### Notations ``` {near F, P} == the property P holds near the canonical filter associated to F P must have the form forall x, Q x. Equivalent to F Q. Prefer this notation when P is an existing statement to be relativised (i.e., has its own definition). \forall x \near F, P x <-> F (fun x => P x). Prefer this notation when the statement forall x, P x does not stand alone. {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 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 "existential", and an unaccessible hypothesis `?H x` and asks the user to prove `(G x)` in this context. Under the hood, it 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 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 user to prove `F H_i`, right now. - `end_near` should be used to close remaining existentials trivially. - `near F => x` poses a variable near `F`, where `F` is a proper filter. It adds to the context a variable `x` that `\is_near F`, i.e., one may assume `H x` for any `H` in `F`. This new variable `x` can be dealt with using `near: x`, as for variables introduced by `near=>`. - `near do tac` does `near=> x; tac; near: x` where `x` is a fresh variable

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

#[global,export] Obligation Tactic := idtac.

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Reserved Notation "{ 'near' x , P }" (at level 0, format "{ 'near' x , P }").
Reserved Notation "'\forall' x '\near' x_0 , P"
  (at level 200, x name, P at level 200,
   format "'\forall' x '\near' x_0 , P").
Reserved Notation "{ 'near' x & y , P }"
  (at level 0, format "{ 'near' x & y , P }").
Reserved Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P"
  (at level 200, x name, y name, P at level 200,
   format "'\forall' x '\near' x_0 & y '\near' y_0 , P").
Reserved Notation "'\forall' x & y '\near' z , P"
  (at level 200, x name, y name, P at level 200,
   format "'\forall' x & y '\near' z , P").
Reserved Notation "F `=>` G" (at level 70, format "F `=>` G").
Reserved Notation "F --> G" (at level 70, format "F --> G").
Reserved Notation "[ 'lim' F 'in' T ]" (format "[ 'lim' F 'in' T ]").
Reserved Notation "[ 'cvg' F 'in' T ]" (format "[ 'cvg' F 'in' T ]").
Reserved Notation "x \is_near F" (at level 10, format "x \is_near F").
Reserved Notation "E @[ x --> F ]"
  (at level 60, x name, format "E @[ x --> F ]").
Reserved Notation "E @[ x \oo ]"
  (at level 60, x name, format "E @[ x \oo ]").
Reserved Notation "f @ F" (at level 60, format "f @ F").
Reserved Notation "E `@[ x --> F ]"
  (at level 60, x name, format "E `@[ x --> F ]").
Reserved Notation "f `@ F" (at level 60, format "f `@ F").

.
   -> set_system U
}.

()
. () of Choice T & isFiltered U T}.
Arguments nbhs {_ _} _ _ : simpl never.

()
. () of Pointed T & isFiltered U T}.

..on (set_system T).
..on (set_system T).
..on (set_system T).
..Build T (set_system T) id.

..

. -> set_system T }.
. T.
  ..Build T T nbhs.
  ..Build T.
..

()
. of Choice T & hasNbhs T}.

()
. of Pointed T & hasNbhs T}.

Definition { : Type} ( : set I) ( : I -> set T) :
  set_system T := [set | exists2 , D i & B i `<=` P].

. ( X) :=
  isFiltered.Build 'M[X]_(m, n) 'M[Z]_(m, n) (fun => filter_from
    [set | forall , nbhs (mx i j) (P i j)]
    (fun => [set : 'M[X]_(m, n) | forall , P i j (my i j)])).

. () := selfFiltered.Build 'M[X]_(m, n).

Definition { : Type}
  ( : set_system T) ( : set_system U) : set_system (T * U) :=
  filter_from (fun => F P.1 /\ G P.2) (fun => P.1 `*` P.2).

Section Near.

Local Notation := (forall , P x : Prop) (at level 0).
Local Notation := (forall , P x y : Prop) (at level 0).
Local Notation := (forall , P x y z: Prop) (at level 0).
Local Notation := (phantom _).

Definition {} { : filteredType X} ( : fX)
    ( : ph {all1 P}) := nbhs x P.

Definition { } { : filteredType X} { : filteredType X'}
  ( : fX) ( : fX') := fun & ph {all2 P} =>
  filter_prod (nbhs x) (nbhs x') (fun => P x.1 x.2).

End Near.

Notation := (@prop_near1 _ _ x _ (inPhantom P)) : type_scope.
Notation := {near x_0, forall , P} : type_scope.
Notation :=
  (@prop_near2 _ _ _ _ x y _ (inPhantom P)) : type_scope.
Notation :=
  {near x_0 & y_0, forall , P} : type_scope.
Notation :=
  {near z & z, forall , P} : type_scope.
Arguments prop_near1 : simpl never.
Arguments prop_near2 : simpl never.

Lemma {} { : set_system T} ( : set T) :
  (\forall \near F, P x) = F P.

Proof.

by []. Qed.

Lemma {} { : set_system T} ( : set T) :
(forall , P x <-> Q x) ->
(\forall \near F, P x) = (\forall \near F, Q x).

Proof.

by move=> /predeqP ->. Qed.

Lemma { : Type} ( : set_system T) : nbhs F = F.

Proof.

by []. Qed.

Module Export .
Definition := (@nbhs_filterE).
End NbhsFilter.

Definition { : Type} ( : set_system T) := G `<=` F.
Notation := (cvg_to F G) : classical_set_scope.

Lemma ( : set_system T) : F `=>` F

Proof.

exact. Qed.

Arguments cvg_refl {T F}.
#[global] Hint Resolve cvg_refl : core.

Lemma ( : set_system T) :
(F `=>` G) -> (G `=>` H) -> (F `=>` H).

Proof.

by move=> FG GH P /GH /FG. Qed.

Notation := (cvg_to (nbhs F) (nbhs G)) : classical_set_scope.
Definition {} ( : set_system T) := T.

Definition { : Type} ( : pfilteredType U) :=
  fun : set_system U => get (fun : T => F --> l).
Notation := (@lim_in _ T (nbhs F)) : classical_set_scope.
Definition { : pnbhsType} ( : set_system T) := [lim F in T].
Notation := (F --> [lim F in T]) : classical_set_scope.
Notation F := (F --> lim F).

Definition := filter_from setT (fun => [set | (N <= n)%N]).
Notation := eventually : classical_set_scope.

Section FilteredTheory.

. ( X1) (Z2 : filteredType X2) :=
  isFiltered.Build (X1 * X2)%type (Z1 * Z2)%type
    (fun => filter_prod (nbhs x.1) (nbhs x.2)).

. ()  :=
  selfFiltered.Build (X1 * X2)%type.

Lemma { : filteredType T} ( : U) ( : U') ( : V) ( : 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.

Lemma { : Type} ( : pfilteredType U) ( : set_system U) :
[cvg F in T] <-> (exists : T, F --> l).

Proof.

by split=> [cvg|/getPex//]; exists [lim F in T]. Qed.

Lemma ( : pnbhsType) ( : set_system T) :
cvg F <-> (exists : T, F --> l).

Proof.

exact: cvg_in_ex. Qed.

Lemma { : Type} ( : pfilteredType U) ( : set_system U) ( : T) :
F --> l -> [cvg F in T].

Proof.

by move=> Fl; apply/cvg_in_ex; exists l. Qed.

Lemma ( : pnbhsType) ( : set_system T) ( : T) : F --> l -> cvg F.

Proof.

exact: cvg_inP. Qed.

Lemma { : Type} ( : pfilteredType U) ( : set_system U) ( : T) :
[cvg F in T] -> [lim F in T] = l -> F --> l.

Proof.

by move=> /[swap]->. Qed.

Lemma ( : pnbhsType) ( : set_system T) ( : T) :
cvg F -> lim F = l -> F --> l.

Proof.

exact: cvg_in_toP. Qed.

Lemma { : Type} ( : pfilteredType U) ( : set_system U) :
~ [cvg F in T] -> [lim F in T] = point.

Proof.

by rewrite /lim_in /=; case xgetP. Qed.

Lemma ( : pnbhsType) ( : set_system T) : ~ cvg F -> lim F = point.

Proof.

exact: dvg_inP. Qed.

Lemma {} ( : pfilteredType U) ( : set_system U) :
[lim F in T] != point -> [cvg F in T].

Proof.

by apply: contra_neqP; apply: dvg_inP. Qed.

Lemma ( : pnbhsType) ( : set_system T) : lim F != point -> cvg F.

Proof.

exact: cvg_inNpoint. Qed.

End FilteredTheory.
Arguments cvg_inP {U T F} l.
Arguments dvg_inP {U} T {F}.
Arguments cvgP {T F} l.
Arguments dvgP {T F}.

Lemma {} { : filteredType U} ( : T) ( : set U) :
nbhs x P = \forall \near x, P x0.

Proof.

by []. Qed.

Lemma {} { : filteredType U} ( : T) ( : set U) :
(\forall \near nbhs x, P x0) = (\forall \near x, P x0).

Proof.

by []. Qed.

Lemma { } ( : set_system U) ( : set_system V) ( : U -> set V) :
{near F & G, forall , P x y} = {near (F, G), forall , P x.1 x.2}.

Proof.

by []. Qed.

Lemma { } ( : set_system U) ( : set_system V) ( : set (U * V)) :
{near F & G, forall , P (x, y)} = {near (F, G), forall , P x}.

Proof.

by symmetry; congr (nbhs _); rewrite predeqE => -[]. Qed.

Definition := (@near2_curry, @near2_pair).

Lemma ( : Type) ( : filteredType X)
( : fX) : forall ,
nbhs x P = @prop_near1 X fX x P (inPhantom (forall , P x)).

Proof.

by []. Qed.

Module Export .
Definition := (@near_nbhs, filter_of_nearI).
End NearNbhs.

Lemma { } ( : set_system U) ( : set_system V) ( : U -> set V) :
(\forall \near F & \near G, P x y) = (\forall \near G & \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.

Filters

Class { : Type} ( : set_system T) := {
   : F setT ;
   : setI_closed F ;
   : forall : set T, P `<=` Q -> F P -> F Q
}.
Global Hint Mode Filter - ! : typeclass_instances.

Class { : Type} ( : set_system T) := {
   : ~ F set0 ;
   : Filter F
}.
Global Existing Instance filter_filter.
Global Hint Mode ProperFilter - ! : typeclass_instances.
Arguments filter_not_empty {T} F {_}.
Hint Extern 0 (~ _ set0) => solve [apply: filter_not_empty] : core.

Lemma ( : Type) : Filter [set: set T].

Proof.

by constructor. Qed.

Lemma ( : set_system T) { : Filter F} ( : set T) :
(exists : set T, exists : F Q, forall : T, Q x -> P x) <-> F P.

Proof.

split; last by exists P.
by move=> [Q [FQ QP]]; apply: (filterS QP).
Qed.

Structure := FilterType {
   :> set_system T;
  _ : Filter filter
}.
Definition ( : filter_on T) : Filter F :=
  let: FilterType _ class := F in class.
Arguments FilterType {T} _ _.
#[global] Existing Instance filter_class.
Coercion filter_filter : ProperFilter >-> Filter.

Structure := PFilterPack {
   :> (T -> Prop) -> Prop;
  _ : ProperFilter pfilter
}.
Definition ( : pfilter_on T) : ProperFilter F :=
  let: PFilterPack _ class := F in class.
Arguments PFilterPack {T} _ _.
#[global] Existing Instance pfilter_class.
Canonical ( : pfilter_on T) :=
  FilterType F (pfilter_class F).
Coercion pfilter_filter_on : pfilter_on >-> filter_on.
Definition {} ( : (T -> Prop) -> Prop)
  { : Filter F} ( : not (F set0)) :=
  PFilterPack F (Build_ProperFilter fN0 fF).
Arguments PFilterType {T} F {fF} fN0.

. (filter_on T).
. (filter_on T).
..Build (filter_on T)
  (FilterType _ (filter_setT T)).
..Build T (filter_on T) (@filter T).

Global Instance ( : filter_on T) : Filter F.

Proof.

by case: F. Qed.

Global Instance ( : pfilter_on T) : ProperFilter F.

Proof.

by case: F. Qed.

Lemma ( : filter_on T) : nbhs F = nbhs (filter F).

Proof.

by []. Qed.

Definition := (@nbhs_simpl, @nbhs_filter_onE).

Lemma ( : filter_on T) ( : set T) :
(\forall \near F, P x) = \forall \near filter F, P x.

Proof.

by []. Qed.

Definition := (@near_simpl, @near_filter_onE).

Program Definition := FilterType [set setT : set T] _.

Next Obligation.

split=> // [_ _ -> ->|Q R sQR QT]; first by rewrite setIT.
by move; rewrite eqEsubset; split => // ? _; apply/sQR; rewrite QT.
Qed.

Canonical trivial_filter_on.

Lemma { : Type} ( : set_system T) :
Filter F -> nbhs F setT.

Proof.

by move=> FF; apply: filterT. Qed.

#[global] Hint Resolve filter_nbhsT : core.

Lemma { : Type} ( : set_system T) : Filter F -> \forall _ \near F, True.

Proof.

by move=> FF; apply: filterT. Qed.

#[global] Hint Resolve nearT : core.

Lemma { : Type} ( : set_system T) :
(forall , F P -> exists , P x) -> ~ F set0.

Proof.

by move=> /(_ set0) ex /ex []. Qed.

Definition { : Type} ( : set_system T)
  ( : forall , F P -> exists , P x)
  ( : Filter F) :=
  Build_ProperFilter (filter_not_empty_ex filter_ex) FF.

Lemma { : Type} ( : set_system T) :
  ~ F set0 -> (forall , F P -> exists , P x).

Proof.

move=> NFset0 P FP; apply: contra_notP NFset0 => nex; suff <- : P = set0 by [].
by rewrite funeqE => x; rewrite propeqE; split=> // Px; apply: nex; exists x.
Qed.

Definition { : Type} ( : set_system T) { : ProperFilter F} :=
filter_ex_subproof (filter_not_empty F).
Arguments filter_ex {T F FF _}.

Lemma { : pointedType} ( : set_system T) { : ProperFilter F}
( : set T) : F P -> P (get P).

Proof.

by move=> /filter_ex /getPex. Qed.

Record ( : set_system T) := InFilter {
: T -> Prop;
: F prop_in_filter_proj
}.

Module Type .
Axiom : forall ( : Type) ( : set_system T), in_filter F -> T -> Prop.
Axiom : t = prop_in_filter_proj.
End PropInFilterSig.
Module : PropInFilterSig.
Definition := prop_in_filter_proj.
Lemma : t = prop_in_filter_proj

Proof.

by []. Qed.

End PropInFilter.
Notation := PropInFilter.t.
Definition := PropInFilter.tE.
Notation := (@PropInFilter.t _ F _ x).
Definition := prop_ofE.

Lemma ( : @in_filter T F) : F (prop_of iF).

Proof.

by rewrite prop_ofE; apply: prop_in_filterP_proj. Qed.

Definition ( : Filter F) : @in_filter T F :=
  InFilter (filterT).
Canonical ( : Filter F) ( : @in_filter T F) :=
  InFilter (filterI (prop_in_filterP_proj P) (prop_in_filterP_proj Q)).

Lemma ( : @in_filter T F) ( : set T) : Filter F ->
  (forall , prop_of P x -> Q x) -> F Q.

Proof.

by move: P => [P FP] FF /=; rewrite prop_ofE /= => /filterS; apply.
Qed.

Fact : unit

Proof.

exact. Qed.

Lemma ( : Prop) : locked_with near_key P -> P.

Proof.

by rewrite unlock. Qed.

Lemma ( : @in_filter T F) ( : set T) ( : Filter F)
( : \forall \near F, Q x) :
locked_with near_key (forall , prop_of (in_filterI FF P (InFilter FQ)) x -> Q x).

Proof.

by rewrite unlock => x /=; rewrite !prop_ofE /= => -[Px]. Qed.

Lemma ( : @in_filter T F) ( : set T) ( : Filter F) :
locked_with near_key (forall , prop_of P x -> G x) ->
locked_with near_key (forall , prop_of (in_filterI FF P Q) x -> G x).

Proof.

rewrite !unlock => FG x /=; rewrite !prop_ofE /= => -[Px Qx].
by have /= := FG x; apply; rewrite prop_ofE.
Qed.

Tactic Notation "near=>" ident(x) := apply: filter_near_of => x ?.

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: near_skip_subproof end.

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.

Ltac under_near i tac := near=> i; tac; near: i.
Tactic Notation "near=>" ident(i) "do" tactic3(tac) := under_near i ltac:(tac).
Tactic Notation "near=>" ident(i) "do" "[" tactic4(tac) "]" := near=> i do tac.
Tactic Notation "near" "do" tactic3(tac) :=
  let i := fresh "i" in under_near i ltac:(tac).
Tactic Notation "near" "do" "[" tactic4(tac) "]" := near do tac.

Ltac end_near := do ?exact: in_filterT.

Ltac done :=
  trivial; hnf; intros; solve
   [ do ![solve [trivial | apply: sym_equal; trivial]
         | discriminate | contradiction | split]
   | match goal with H : ~ _ |- _ => solve [case H; trivial] end
   | match goal with |- ?x \is_near _ => near: x; apply: prop_ofP end ].

Lemma ( : Type) ( : filteredType U) ( : fT) ( : Prop) :
  ProperFilter (nbhs x) -> (\forall \near x, P) -> P.

Proof.

by move=> FF nP; have [] := @filter_ex _ _ FF (fun=> P). Qed.

Arguments have_near {U fT} x.

Tactic Notation "near" constr(F) "=>" ident(x) :=
apply: (have_near F); near=> x.

Lemma ( : set_system T) ( : F P) ( : T)
( : prop_of (InFilter FP) x) : P x.

Proof.

by move: Px; rewrite prop_ofE. Qed.

Arguments near {T F P} FP x Px.

Lemma { : Type} { : set_system T} ( : T -> Prop) :
Filter F -> (forall , P x) -> (\forall \near F, P x).

Proof.

by move=> FF FP; apply: filterS filterT. Qed.

Lemma { : Type} { : set_system T} :
Filter F -> forall : set T, (forall , P x) -> F P.

Proof.

by move=> [FT _ +] P fP => /(_ setT); apply. Qed.

Lemma ( : Type) ( : set_system T) :
Filter F -> forall : set T, F (fun => P x -> Q x) -> F P -> F Q.

Proof.

by move=> FF P Q subPQ FP; near=> x do suff: P x.
Unshelve. all: by end_near. Qed.

Lemma ( : Type) ( : set_system T) :
Filter F -> forall : set T, F (fun => 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 ( : Type) ( : set_system T) :
Filter F -> forall : set T, F (fun => 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 ( : Type) ( : set_system T) :
Filter F -> forall : set T, (forall , P x -> Q x -> R x) ->
F P -> F Q -> F R.

Proof.

by move=> ? ? ? ? ?; apply: filter_app2; apply: filterE. Qed.

Lemma ( : Type) ( : set_system T) :
Filter F -> forall : set T, (forall , 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 { : Type} {} {: @ProperFilter T F} ( : Prop) :
F (fun=> P) -> P.

Proof.

by move=> FP; case: (filter_ex FP). Qed.

Lemma { : Type} ( : set I) ( : I -> set T) ( : I) :
D i -> filter_from D B (B i).

Proof.

by exists i. Qed.

Lemma { : Type} ( : set_system T) ( : T -> Prop) ( : set T) :
Filter F -> F S -> {in S, forall , P x} -> \forall \near F, P x.

Proof.

by move=> FF FS SP; apply: (@filterS _ F _ S) => // x /mem_set /SP.
Qed.

Lemma { : Type} ( : T -> Prop) : Filter F ->
(\forall \near F, b1 x /\ b2 x) <->
(\forall \near F, b1 x) /\ (\forall \near F, b2 x).

Proof.

move=> FF; split=> [H|[H1 H2]]; first by split; apply: filterS H => ? [].
by apply: filterS2 H1 H2.
Qed.

Lemma { } { : set_system T} { : set_system U}
   { : Filter F} { : Filter G} ( : T -> U -> Prop) :
  (\forall \near F & \near G, P x y) ->
  \forall \near F, \forall \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 (_, _)).
Qed.

Lemma ( : set_system T) ( : set_system U)
  { : Filter F} { : Filter G} ( : set (T * U)) :
  (exists2 : set T * set U, F Q.1 /\ G Q.2
     & forall ( : T) ( : U), Q.1 x -> Q.2 y -> P (x, y))
   <-> \forall \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 { : Type} ( : set_system T) ( : set_system U)
{ : ProperFilter F} { : ProperFilter G} ( : set T) ( : set U) :
F P -> G Q -> exists : T, exists2 : 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 { : Type} ( : set I) ( : I -> set T) ( : set_system T) :
Filter F -> F `=>` filter_from D B <-> forall , 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 { : Type} ( : I -> set T) ( : set_system T) :
Filter F -> F `=>` filter_from setT B <-> forall , F (B i).

Proof.

by move=> FF; rewrite filter_fromP; split=> [P i|P i _]; apply: P. Qed.

Lemma { : Type} ( : set I) ( : I -> set T) :
  (exists : I, D i) ->
  (forall , D i -> D j -> exists2 , D k & B k `<=` B i `&` B j) ->
  Filter (filter_from D B).

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.
Qed.

Lemma { : Type} ( : I -> set T) :
  (exists _ : I, True) ->
  (forall , exists , 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 { : Type} ( : set I) ( : I -> set T) :
  Filter (filter_from D B) ->
  (forall , D i -> B i !=set0) ->
  ProperFilter (filter_from D B).

Proof.

move=> FF BN0; apply: Build_ProperFilter_ex => P [i Di BiP].
by have [x Bix] := BN0 _ Di; exists x; apply: BiP.
Qed.

Global Instance : ProperFilter eventually.

Proof.

eapply @filter_from_proper; last by move=> i _; exists i => /=.
apply: filter_fromT_filter; first by exists 0%N.
move=> i j; exists (maxn i j) => n //=.
by rewrite geq_max => /andP[ltin ltjn].
Qed.

Canonical := FilterType eventually _.
Canonical := PFilterType eventually (filter_not_empty _).

Lemma ( : choiceType) ( : {fset I}) ( : I -> set T)
  ( : set_system T) :
  Filter F -> (forall , i \in D -> F (f i)) ->
  F (\bigcap_( in [set` D]) f i).

Proof.

move=> FF FfD.
suff: F [set | forall , i \in enum_fset D -> f i p] by [].
have {FfD} : forall , 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 | forall , 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.
Qed.

Lemma ( : finType) ( : I -> set T) ( : set_system T) :
Filter F -> (forall : I, \forall \near F, f i x) ->
\forall \near F, forall , f i x.

Proof.

move=> FF fIF; apply: filterS (@filter_bigI T I [fset in I]%fset f F FF _).
by move=> x fIx i; have := fIx i; rewrite /= inE/=; apply.
by move=> i; rewrite inE/= => _; apply: (fIF i).
Qed.

Lemma [ : Type] [ : Prop] [ : set T] [ : set_system T] :
Filter F -> (P -> \forall \near F, f x) -> \forall \near F, P -> f x.

Proof.

move=> ? PF; near do move=> /asboolP.
by case: asboolP=> [/PF|_]; by [apply: filterS|apply: nearW].
Unshelve. all: by end_near. Qed.

Limits expressed with filters

Definition { : Type} ( : T -> U) ( : set_system T) : set_system U :=
[set | F (f @^-1` P)].
Arguments fmap _ _ _ _ _ /.

Lemma { : Type} ( : U -> V)
( : set_system U) ( : set V) : fmap f F P = F (f @^-1` P).

Proof.

by []. Qed.

Notation :=
  (fmap (fun => E) (nbhs F)) : classical_set_scope.
Notation :=
  (fmap (fun => E) \oo) : classical_set_scope.
Notation := (fmap f (nbhs F)) : classical_set_scope.

Notation F := (lim (F @ \oo)).
Notation F := (cvg (F @ \oo)).

Global Instance ( : T -> U) ( : set_system T) :
  Filter F -> Filter (f @ F).

Proof.

move=> FF; constructor => [|P Q|P Q PQ]; rewrite ?fmapE //=.
- exact: filterT.
- exact: filterI.
- by apply: filterS=> ?/PQ.
Qed.

Global Instance ( : T -> U) ( : set_system T) :
ProperFilter F -> ProperFilter (f @ F).

Proof.

by move=> FF; apply: Build_ProperFilter; rewrite fmapE preimage_set0.
Qed.

Definition { : Type} ( : T -> set U) ( : set_system T) :
    set_system _ :=
  [set | \forall \near F, exists , f x y /\ P y].

Notation :=
  (fmapi (fun => E) (nbhs F)) : classical_set_scope.
Notation := (fmapi f (nbhs F)) : classical_set_scope.

Lemma { : Type} ( : U -> set V)
  ( : set_system U) ( : set V) :
  fmapi f F P = \forall \near F, exists , f x y /\ P y.

Proof.

by []. Qed.

Global Instance ( : T -> set U) ( : set_system T) :
{near F, is_totalfun f} -> Filter F -> Filter (f `@ F).

Proof.

move=> f_totalfun FF; rewrite /fmapi; apply: Build_Filter.
- by apply: filterS f_totalfun => x [[y Hy] H]; exists y.
- move=> /= P Q 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.
  by have [//|y [fxy /subPQ Qy]] := near FP x; exists y.
Unshelve. all: by end_near. Qed.

#[global] Typeclasses Opaque fmapi.

Global Instance
   ( : T -> U -> Prop) ( : set_system T) :
  {near F, is_totalfun f} ->
  ProperFilter F -> ProperFilter (f `@ F).

Proof.

move=> f_totalfun FF; apply: Build_ProperFilter_ex.
by move=> P; rewrite /fmapi/= => /filter_ex [x [y [??]]]; exists y.
exact: fmapi_filter.
Qed.

Lemma ( : set_system T) : x @[ --> F] --> F.

Proof.

exact. Qed.

Arguments cvg_id {T F}.

Lemma { } ( : B -> C) ( : A -> B) :
Filter F -> (f \o g)%FUN @ F = f @ (g @ F).

Proof.

by []. Qed.

Lemma ( : U -> V) ( : set_system U) :
f @ F = [set : set _ | \forall \near F, P (f x)].

Proof.

by []. Qed.

Lemma ( : set_system U) ( : U -> V) :
F --> G -> f @ F --> f @ G.

Proof.

by move=> FG P /=; exact: FG. Qed.

Arguments cvg_app {U V F G} _.

Lemma ( : set_system U) ( : U -> set V) :
F --> G -> f `@ F --> f `@ G.

Proof.

by move=> FG P /=; exact: FG. Qed.

Lemma ( : T -> U) ( : U -> V)
( : set_system T) ( : set_system U) ( : set_system V) :
f @ F `=>` G -> g @ G `=>` H -> g \o f @ F `=>` H.

Proof.

by move=> fFG gGH; apply: cvg_trans gGH => P /fFG. Qed.

Arguments cvg_comp {T U V} f g {F G H}.

Lemma ( : T -> U) ( : U -> set V)
( : set_system T) ( : set_system U) ( : set_system V) :
f @ F `=>` G -> g `@ G `=>` H -> g \o f `@ F `=>` H.

Proof.

by move=> fFG gGH; apply: cvg_trans gGH => P /fFG. Qed.

Lemma { } { : set_system T} { : Filter F} ( : T -> U) :
{near F, f =1 g} -> g @ F `=>` f @ F.

Proof.

by move=> eq_fg P /=; apply: filterS2 eq_fg => x /= <-. Qed.

Lemma { } { : set_system T} { : Filter F} ( : T -> U) :
{near F, f =1 g} -> f @ F = g @ F.

Proof.

move=> fg; apply/seteqP; split; apply: near_eq_cvg => //.
by near do symmetry.
Unshelve. all: by end_near. Qed.

Lemma ( : Type) ( : set_system T) ( : T -> U) ( : set_system U) :
f =1 g -> (f @ F --> x) = (g @ F --> x).

Proof.

by move=> /funext->. Qed.

Lemma ( : Type) ( : pnbhsType) ( : set_system T)
( : T -> U) :
Filter F -> {near F, f =1 g} -> cvg (f x @[ --> F]) -> cvg(g x @[ --> F]).

Proof.

by move=> FF /near_eq_cvg_eq ->. Qed.

Lemma ( : Type) ( : pfilteredType U) ( : set_system T)
( : T -> U) :
f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT].

Proof.

by move=> /funext ->. Qed.

Lemma ( : Type) ( : pnbhsType) ( : set_system T) ( : T -> U) :
f =1 g -> cvg (f @ F) = cvg (g @ F).

Proof.

by move=> /funext->. Qed.

Lemma ( : Type) ( : pnbhsType) { : set_system T} { : Filter F}
( : T -> U) :
{near F, f =1 g} -> lim (f @ F) = lim (g @ F).

Proof.

by move=> /near_eq_cvg_eq ->. Qed.

Lemma { } { : set_system T} { : Filter F} ( : 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]].
by exists y; rewrite -eq_fg.
Qed.

Lemma ( : Type) ( : T -> U) ( : set_system T) ( : set_system U) :
Filter F -> ProperFilter G ->
(\forall \near G, \forall \near F, f x = y) -> f @ F --> G.

Proof.

move=> FF FG fFG P /= GP; rewrite !near_simpl; apply: (have_near G).
by apply: filter_app fFG; near do apply: filterS => x /= ->.
Unshelve. all: by end_near. Qed.

Definition ( : nbhsType) ( : T) ( : T -> U) :=
  (f%function @ x --> f%function x).
Notation f := (forall , continuous_at x f).

Lemma ( : nbhsType) ( : R -> S) ( : S -> T) :
  {for x, continuous f} -> {for (f x), continuous g} ->
  {for x, continuous (g \o f)}.

Proof.

exact: cvg_comp. Qed.

.
  () (S : pred V) U & SubChoice V S U & Nbhs U := {
  continuous_valE : continuous (val : U -> V)
}.

()
. () (S : pred V) :=
  { of SubChoice V S U & Nbhs U & isSubNbhs V S U}.

Lemma ( : nbhsType) ( : T -> T') ( : T) ( : T' -> Prop) :
    {for x, continuous f} ->
  (\forall \near f x, P y) -> (\forall \near x, P (f x0)).

Proof.

exact. Qed.

Arguments near_fun {T T'} f x.

Definition { : Type} ( : set T) : set_system T :=
[set : set T | forall , A x -> P x].
Arguments globally {T} A _ /.

Lemma { : Type} ( : set T) : globally set0 A

Proof.

by []. Qed.

Global Instance { : Type} ( : set T) :
Filter (globally A).

Proof.

constructor => //= P Q; last by move=> PQ AP x /AP /PQ.
by move=> AP AQ x Ax; split; [apply: AP|apply: AQ].
Qed.

Global Instance { : Type} ( : set T) :
A a -> ProperFilter (globally A).

Proof.

by move=> Aa; apply: Build_ProperFilter => /(_ a); exact. Qed.

Specific filters

Section frechet_filter.
Variable : Type.

Definition := [set : set T | finite_set (~` S)].

Global Instance : infinite_set [set: T] ->
ProperFilter frechet_filter.

Proof.

move=> infT; rewrite /frechet_filter.
constructor; first by rewrite /= setC0; exact: infT.
constructor; first by rewrite /= setCT.
- by move=> ? ?; rewrite /= setCI finite_setU.
- by move=> P Q PQ; exact/sub_finite_set/subsetC.
Qed.

End frechet_filter.

Global Instance : ProperFilter (@frechet_filter nat).

Proof.

by apply: frechet_properfilter; exact: infinite_nat. Qed.

Filters for pairs

Global Instance ( : set_system T) ( : set_system U) :
Filter F -> Filter G -> Filter (filter_prod F G).

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] [/= [??] []].
Qed.

Canonical ( : filter_on T) ( : filter_on U) :=
  FilterType (filter_prod F G) (filter_prod_filter _ _).

Global Instance { : Type}
  { : (T1 -> Prop) -> Prop} { : (T2 -> Prop) -> Prop}
  { : ProperFilter F} { : ProperFilter G} :
  ProperFilter (filter_prod F G).

Proof.

apply: filter_from_proper => -[A B] [/=FA GB].
by have [[x ?] [y ?]] := (filter_ex FA, filter_ex GB); exists (x, y).
Qed.

Lemma { } { : set_system T} { : set_system U}
{ : Filter G} ( : set T) :
(\forall \near F, P x) -> \forall \near F & _ \near G, P x.

Proof.

by move=> FP; exists (P, setT)=> //= [|[?? []//]]; split=> //; exact: filterT.
Qed.

Lemma { } { : set_system T} { : set_system U}
{ : Filter F} ( : set U) :
(\forall \near G, P y) -> \forall _ \near F & \near G, P y.

Proof.

by move=> FP; exists (setT, P)=> //= [|[?? []//]]; split=> //; exact: filterT.
Qed.

Program Definition { } { : set_system T} { : set_system U}
( : in_filter F) ( : in_filter G) : in_filter (filter_prod F G) :=
@InFilter _ _ (fun => prop_of P x.1 /\ prop_of Q x.2) _.

Next Obligation.

move=> T U F G P Q.
by exists (prop_of P, prop_of Q) => //=; split; exact: prop_ofP.
Qed.

Lemma { } { : set_system T} { : set_system U}
{ : Filter F} { : Filter G} ( : in_filter F) ( : in_filter G) :
prop_of P x.1 -> prop_of Q x.2 -> prop_of (in_filter_prod P Q) x.

Proof.

by case: x=> x y; do ?rewrite prop_ofE/=. Qed.

Lemma { } { : Filter G} : (@fst T U) @ filter_prod F G --> F.

Proof.

by move=> P; exact: filter_prod1. Qed.

Lemma { } { : Filter F} : (@snd T U) @ filter_prod F G --> G.

Proof.

by move=> P; exact: filter_prod2. Qed.

Lemma { } ( : T -> U) ( : set_system T) ( : set U) :
(\forall \near f @ F, P y) = (\forall \near F, P (f x)).

Proof.

by []. Qed.

Lemma { } ( : T -> U) ( : T' -> U')
      ( : set_system T) ( : set_system T') ( : U -> set U') :
  Filter F -> Filter G ->
  (\forall \near f @ F & \near g @ G, P y y') =
  (\forall \near F     & \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 !nbhs_simpl /fmap /=; split.
  by apply: filterS fFA=> x Ax; exists x.
by apply: filterS fGB => x Bx; exists x.
Qed.

Lemma { } ( : T -> set U) ( : set_system T) ( : set U) :
(\forall \near f `@ F, P y) = (\forall \near F, exists , f x y /\ P y).

Proof.

by []. Qed.

Lemma ( : Type) ( : set_system T) ( : set_system T') :
   Filter F -> Filter F' ->
   forall ( : set T) ( : set T') ( : set (T * T')),
   (forall , P x -> P' x' -> Q (x, x')) -> F P /\ F' P' ->
   filter_prod F F' Q.

Proof.

by move=> FF FF' P P' Q PQ [FP FP'];
near=> x do [have := PQ x.1 x.2; rewrite -surjective_pairing; apply];
[apply: cvg_fst | apply: cvg_snd].
Unshelve. all: by end_near. Qed.

Lemma ( : Type) ( : set_system T) ( : set_system T') :
   Filter F -> Filter F' ->
   forall ( : @in_filter T F) ( : @in_filter T' F') ( : set (T * T')),
   (forall , prop_of P x -> prop_of P' x' -> Q (x, x')) ->
   filter_prod F F' Q.

Proof.

move=> FF FF' [P FP] [P' FP'] Q PQ; rewrite prop_ofE in FP FP' PQ.
by exists (P, P') => //= -[t t'] [] /=; exact: PQ.
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.

Module Export .
Definition := (@near_simpl, @near_map, @near_mapi, @near_map2).
Ltac near_simpl := rewrite ?near_simpl.
End NearMap.

Lemma { : numDomainType} ( : pred R) ( : set_system R) :
  (\forall \near - x @[ --> F], (P \o -%R) x) = \forall \near F, P x.

Proof.

by rewrite near_simpl/= !nearE; under eq_fun do rewrite opprK. Qed.

Lemma { } { : set_system U} { : set_system V}
  { : Filter F} { : Filter G} { : Filter H} ( : T -> U) ( : T -> V) :
  f @ F --> G -> g @ F --> H ->
  (f x, g x) @[ --> F] --> (G, H).

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].
Unshelve. all: by end_near. Qed.

Lemma { }
  { : set_system T} { : set_system U} { : set_system V} { : set_system W}
  { : Filter F} { : Filter G} { : Filter H}
  ( : T -> U) ( : T -> V) ( : U -> V -> W) :
  f @ F --> G -> g @ F --> H ->
  h (fst x) (snd x) @[ --> (G, H)] --> I ->
  h (f x) (g x) @[ --> F] --> I.

Proof.

by move=> fFG gFH hGHI P /= IP; apply: cvg_pair (hGHI _ IP). Qed.

Arguments cvg_comp2 {T U V W F G H I FF FG FH f g h} _ _ _.
Definition := @cvg_comp2.

Restriction of a filter to a domain

Section within.
Context { : Type}.
Implicit Types (D : set T) (F : set_system T).

Definition : set_system T := [set | {near F, D `<=` P}].
Arguments within : simpl never.

Lemma ( : set T) :
(\forall \near within D F, P x) = {near F, D `<=` P}.

Proof.

by []. Qed.

Lemma : Filter F -> within D F D.

Proof.

by move=> FF; rewrite /within/=; apply: filterE. Qed.

Lemma : Filter F -> \forall \near within D F, D x.

Proof.

exact: withinT. Qed.

Lemma {} { : Filter F} : within D F --> F.

Proof.

by move=> P; apply: filterS. Qed.

Lemma {} { : Filter F} : within setT F = F.

Proof.

rewrite eqEsubset /within; split => X //=;
by apply: filter_app => //=; apply: nearW => // x; apply.
Qed.

End within.

Lemma ( : Type) { : set_system T} { : Filter F}
{ : set_system U} { : Filter G} ( : T -> U) ( : set U) :
(f @ F --> within A G) <-> (f @ F --> G /\ \forall \near F, A (f x)).

Proof.

split.
- move=> fFAG; split.
  + exact/(cvg_trans fFAG)/cvg_within.
  + by apply/fFAG; exact: withinT.
- move=> [+ fA] B => /[apply]; rewrite nbhs_simpl.
  by apply: filterS2 fA => t ?; exact.
Unshelve. all: by end_near. Qed.

Global Instance : Filter F -> Filter (@within T D F).

Proof.

move=> FF; rewrite /within; constructor => /=.
- exact: filterE.
- by move=> P Q/=; apply: filterS2 => x DP DQ Dx; split; [exact: DP|exact: DQ].
- by move=> P Q subPQ; apply: filterS => x DP /DP /subPQ.
Qed.

#[global] Typeclasses Opaque within.

Canonical ( : filter_on T) :=
  FilterType (within D F) (within_filter _ _).

Lemma { : Type} { : set_system T} { : Filter F}
    { : set_system U} { : Filter G} ( : T -> U) ( : set T) ( : set U) :
  (\forall \near F, A x -> B (f x)) -> f @ F --> G ->
  f @ within A F --> within B G.

Proof.

move=> near_hom fFG; apply/cvg_to_withinP; split.
- by apply: cvg_trans fFG; apply: cvg_app; exact: cvg_within.
- by rewrite near_withinE.
Qed.

Lemma ( : choiceType) ( : {fset I}) ( : I -> set T)
    ( : set_system T) ( : set T) :
  Filter F -> (forall , i \in D -> F [set | P j -> f i j]) ->
  F ([set | P j -> (\bigcap_( in [set` D]) f i) j]).

Proof.

move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed.

Definition {} ( : set_system T) ( : set T) :=
[set : set { | D x} | F [set | forall : D x, P (exist _ x Dx)]].
Arguments subset_filter {T} F D _.

Global Instance ( : set T) :
Filter F -> Filter (subset_filter F D).

Proof.

move=> FF; constructor; rewrite /subset_filter/=.
- exact: filterE.
- by move=> P Q/=; exact: filterS2.
- by move=> P Q subPQ; apply: filterS => R PD Dx; apply: subPQ.
Qed.

#[global] Typeclasses Opaque subset_filter.

Lemma { } { : Filter F} ( : set T) :
(forall , F P -> ~ ~ exists , D x /\ P x) ->
ProperFilter (subset_filter F D).

Proof.

move=> DAP; apply: Build_ProperFilter; rewrite /subset_filter => subFD.
by have /(_ subFD) := DAP (~` D); apply => -[x [dx /(_ dx)]].
Qed.

Section NearSet.
Context { : Type} ( : set_system Y) ( : ProperFilter F).

Definition : set_system (set Y) := filter_from
  [set | [/\ M `<=` F,
    (forall , M E1 -> F E2 -> E2 `<=` E1 -> M E2) & M !=set0 ] ]
  id.

Global Instance : ProperFilter powerset_filter_from.

Proof.

split.
  by move=> [W [_ _ [N +]]]; rewrite subset0 => /[swap] ->; apply.
apply: filter_from_filter.
  by exists F; split => //; exists setT; exact: filterT.
move=> M N /= [entM subM [M0 MM0]] [entN subN [N0 NN0]].
exists [set | exists , [/\ M P, N Q & E = P `&` Q] ]; first split.
- by move=> ? [? [? [? ? ->]]]; apply: filterI; [exact: entM | exact: entN].
- move=> ? E2 [P [Q [MP MQ ->]]] entE2 E2subPQ; exists E2, E2.
  split; last by rewrite setIid.
  + by apply: (subM _ _ MP) => // ? /E2subPQ [].
  + by apply: (subN _ _ MQ) => // ? /E2subPQ [].
- by exists (M0 `&` N0), M0, N0.
- move=> E /= [P [Q [MP MQ ->]]]; have entPQ : F (P `&` Q).
    by apply: filterI; [exact: entM | exact: entN].
  by (split; [apply: (subM _ _ MP) | apply: (subN _ _ MQ)]) => // ? [].
Qed.

Lemma : \forall \near powerset_filter_from, F E.

Proof.

by exists F => //; split => //; exists setT; exact: filterT. Qed.

Lemma ( : set Y) : F E ->
\forall \near powerset_filter_from, E' `<=` E.

Proof.

move=> entE; exists [set | F E' /\ E' `<=` E]; last by move=> ? [].
split; [by move=> E' [] | | by exists E; split].
by move=> E1 E2 [] ? subE ? ?; split => //; exact: subset_trans subE.
Qed.

Lemma ( : set Y -> Prop) :
(forall , A `<=` B -> P B -> P A) ->
(\forall \near powerset_filter_from, P U) <-> exists2 , F U & P U.

Proof.

move=> Psub; split=> [[M [FM ? [U MU]]] MsubP|[U FU PU]].
by exists U; [exact: FM | exact: MsubP].
exists [set | F V /\ V `<=` U]; last by move=> V [_] /Psub; exact.
split=> [E [] //| |]; last by exists U; split.
by move=> E1 E2 [F1 E1U F2 E2subE1]; split => //; exact: subset_trans E1U.
Qed.

Lemma :
F C -> powerset_filter_from [set | F W /\ W `<=` C].

Proof.

move=> FC; exists [set | F W /\ W `<=` C] => //; split; first by move=> ? [].
by move=> A B [_ AC] FB /subset_trans/(_ AC).
by exists C; split.
Qed.

End NearSet.

Lemma { : Type} ( : T -> U) ( : set_system T)
  ( : set U -> Prop) :
  ProperFilter F ->
  (\forall \near powerset_filter_from (f x @[ --> F]), P y) ->
  (\forall \near powerset_filter_from F, P (f @` y)).

Proof.

move=> FF [] G /= [Gf Gs [D GD GP]].
have PpF : ProperFilter (powerset_filter_from F).
  exact: powerset_filter_from_filter.
have /= := Gf _ GD; rewrite nbhs_simpl => FfD.
near=> M; apply: GP; apply: (Gs D) => //.
  apply: filterS; first exact: preimage_image.
  exact: (near (near_small_set _) M).
have : M `<=` f @^-1` D by exact: (near (small_set_sub FfD) M).
by move/image_subset/subset_trans; apply; exact: image_preimage_subset.
Unshelve. all: by end_near. Qed.

Lemma { : Type} ( : T -> U) ( : set_system T)
  ( : set U -> Prop) :
  (forall , X `<=` Y -> P Y -> P X) ->
  ProperFilter F ->
  (\forall \near powerset_filter_from F, P (f @` y)) =
  (\forall \near powerset_filter_from (f x @[ --> F]), P y).

Proof.

move=> Pmono FF; rewrite propeqE; split; last exact: near_powerset_map.
case=> G /= [Gf Gs [D GD GP]].
have PpF : ProperFilter (powerset_filter_from (f x @[-->F])).
exact: powerset_filter_from_filter.
have /= := Gf _ GD; rewrite nbhs_simpl => FfD; have ffiD : fmap f F (f@` D).
by rewrite /fmap /=; apply: filterS; first exact: preimage_image.
near=> M; have FfM : fmap f F M by exact: (near (near_small_set _) M).
apply: (@Pmono _ (f @` D)); first exact: (near (small_set_sub ffiD) M).
exact: GP.
Unshelve. all: by end_near. Qed.

Section PrincipalFilters.

Definition { : Type} ( : X) : set_system X :=
globally [set x].

we introducing an alias for pointed types with principal filters

Definition ( : Type) : Type := P.
. () :=
  Choice.copy (principal_filter_type P) P.
. () :=
  Pointed.on (principal_filter_type P).
. () :=
  hasNbhs.Build (principal_filter_type P) principal_filter.
. () :=
  Filtered.on (principal_filter_type P).

Lemma {} ( : X) ( : set X) : principal_filter x W <-> W x.

Proof.

by split=> [|? ? ->]; [exact|]. Qed.

Lemma {} ( : X) : ProperFilter (principal_filter x).

Proof.

exact: globally_properfilter. Qed.

..Build bool principal_filter.

End PrincipalFilters.

Section UltraFilters.

Class ( : set_system T) := {
  #[global] :: ProperFilter F ;
   : forall : set_system T, ProperFilter G -> F `<=` G -> G = F
}.

Lemma ( : set_system T) :
  ProperFilter F -> exists , UltraFilter G /\ F `<=` G.

Proof.

move=> FF.
set filter_preordset := ({ : set_system T & ProperFilter G /\ F `<=` G}).
set preorder :=
  fun : {classic filter_preordset} => `[< projT1 G1 `<=` projT1 G2 >].
suff [G Gmax] : exists : {classic filter_preordset}, premaximal preorder G.
  have [GF sFG] := projT2 G; exists (projT1 G); split; last exact: sFG.
  split; [exact: GF|move=> H HF sGH].
  have sFH : F `<=` H by apply: subset_trans sGH.
  have sHG : preorder (existT _ H (conj HF sFH)) G.
    by move/asboolP in sGH; exact: (Gmax (existT _ H (conj HF sFH)) sGH).
  by rewrite predeqE => A; split; [move/asboolP : sHG; exact|exact: sGH].
have sFF : F `<=` F by [].
apply: (ZL_preorder (existT _ F (conj FF sFF))).
- by move=> t; exact/asboolP.
- move=> r s t; rewrite /preorder => /asboolP sr /asboolP st.
  exact/asboolP/(subset_trans _ st).
- move=> A Atot; have [[G AG] | A0] := pselect (A !=set0); 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_( in A) projT1 H).
    have sFUA : F `<=` \bigcup_( in A) projT1 H.
      by move=> B FB; exists G => //; exact: sFG.
    exists (existT _ (\bigcup_( in A) projT1 H) (conj UAF sFUA)) => H AH.
    by apply/asboolP => B HB /=; exists H.
  apply: Build_ProperFilter_ex.
    by move=> B [H AH HB]; have [HF _] := projT2 H; exact: (@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.
      by move/asboolP : sHBC; exact.
    * exists HB => //; have [HBF _] := projT2 HB; apply: filterI HBB _.
      by move/asboolP : sHCB; exact.
  + move=> B C SBC [H AH HB]; exists H => //; have [HF _] := projT2 H.
    exact: filterS HB.
Qed.

Lemma ( : Type) ( : T -> U) ( : set_system T) :
Filter F -> f @` setT = setT -> Filter [set f @` A | in F].

Proof.

move=> FF fsurj; split.
- by exists setT => //; apply: filterT.
- move=> _ _ [A FA <-] [B FB <-].
  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.
- 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.

Lemma ( : Type) ( : T -> U) ( : set_system T) :
ProperFilter F -> f @` setT = setT -> ProperFilter [set f @` A | in F].

Proof.

move=> FF fsurj; apply: Build_ProperFilter_ex; last exact: filter_image.
by move=> _ [A FA <-]; have /filter_ex [p Ap] := FA; exists (f p), p.
Qed.

Lemma { : Type} ( : T) :
UltraFilter (principal_filter x).

Proof.

split=> [|G [G0 xG] FG]; first exact: principal_filter_proper.
rewrite eqEsubset; split => // U GU; apply/principal_filterP.
have /(filterI GU): G [set x] by exact/FG/principal_filterP.
by rewrite setIC set1I; case: ifPn => // /[!inE].
Qed.

Lemma ( : set_system T) ( : set T) :
UltraFilter F -> F A \/ F (~` A).

Proof.

move=> FU; case: (pselect (F (~` A))) => [|nFnA]; first by right.
left; suff : ProperFilter (filter_from (F `|` [set A `&` B | in F]) id).
  move=> /max_filter <-; first by move=> B FB; exists B => //; left.
  by exists A => //; right; exists setT; [exact: filterT|rewrite setIT].
apply: filter_from_proper; last first.
  move=> B [|[C FC <-]]; first exact: filter_ex.
  apply: contrapT => /asboolP; rewrite asbool_neg => /forallp_asboolPn AC0.
  by apply: nFnA; apply: filterS FC => p Cp Ap; exact: (AC0 p).
apply: filter_from_filter.
  by exists A; right; exists setT; [exact: filterT|rewrite setIT].
move=> B C [FB|[DB FDB <-]].
  move=> [FC|[DC FDC <-]]; first by exists (B `&` C)=> //; left; exact: filterI.
  exists (A `&` (B `&` DC)); last by rewrite setICA.
  by right; exists (B `&` DC) => //; exact: filterI.
move=> [FC|[DC FDC <-]].
  exists (A `&` (DB `&` C)); last by rewrite setIA.
  by right; exists (DB `&` C) => //; exact: filterI.
exists (A `&` (DB `&` DC)); last by move=> ??; rewrite setIACA setIid.
by right; exists (DB `&` DC) => //; exact: filterI.
Qed.

Lemma ( : Type) ( : T -> U) ( : set_system T) :
UltraFilter F -> f @` setT = setT -> UltraFilter [set f @` A | in F].

Proof.

move=> FU fsurj; split; first exact: proper_image.
move=> G GF sfFG; rewrite predeqE => A; split; last exact: sfFG.
move=> GA; exists (f @^-1` A); last by rewrite image_preimage.
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 exact: filterI.
Qed.

End UltraFilters.

Section filter_supremums.

Global Instance { : Type} ( : set_system T) :
Filter (smallest Filter F).

Proof.

split.
- by move=> G [? _]; exact: filterT.
- by move=> ? ? sFP sFQ ? [? ?]; apply: filterI; [exact: sFP | exact: sFQ].
- by move=> ? ? /filterS + sFP ? [? ?]; apply; exact: sFP.
Qed.

Fixpoint { : Type} ( : set_system T) ( : nat) :=
  if n is m.+1
  then [set P `&` Q |
     in filterI_iter F m & in filterI_iter F m]
  else setT |` F.

Lemma { : Type} ( : set_system T) :
  {homo filterI_iter F : / (i <= j)%N >-> i `<=` j}.

Proof.

move=> + j; elim: j; first by move=> i; rewrite leqn0 => /eqP ->.
move=> j IH i; rewrite leq_eqVlt => /predU1P[->//|].
by move=> /IH/subset_trans; apply=> A ?; do 2 exists A => //; rewrite setIid.
Qed.

Lemma { : Type} ( : set_system T) :
smallest Filter F = filter_from (\bigcup_ (filterI_iter F n)) id.

Proof.

rewrite eqEsubset; split.
  apply: smallest_sub; first last.
    by move=> A FA; exists A => //; exists O => //; right.
  apply: filter_from_filter; first by exists setT; exists O => //; left.
  move=> P Q [i _ sFP] [j _ sFQ]; exists (P `&` Q) => //.
  exists (maxn i j).+1 => //=; exists P.
    by apply: filterI_iter_sub; first exact: leq_maxl.
  by exists Q => //; apply: filterI_iter_sub; first exact: leq_maxr.
move=> + [+ [n _]]; elim: n => [A B|n IH/= A B].
  move=> [-> /[!(@subTset T)] ->|]; first exact: filterT.
  by move=> FB /filterS; apply; apply: sub_gen_smallest.
move=> [P sFP] [Q sFQ] PQB /filterS; apply; rewrite -PQB.
by apply: (filterI _ _); [exact: (IH _ _ sFP)|exact: (IH _ _ sFQ)].
Qed.

Definition ( : choiceType) ( : set I) ( : I -> set T) :=
  [set \bigcap_( in [set` D']) f i |
     in [set : {fset I} | {subset A <= D}]].

Lemma ( : choiceType) ( : set I) ( : I -> set T) :
  \bigcup_( in open_finI_from D f) A = setT.

Proof.

rewrite predeqE => t; split=> // _; exists setT => //.
by exists fset0 => //; rewrite set_fset0 bigcap_set0.
Qed.

Lemma ( : choiceType) ( : set I) ( : I -> set T) :
D i -> open_finI_from D f (f i).

Proof.

move=> Di; exists [fset i]%fset; first by move=> ?; rewrite !inE => /eqP ->.
by rewrite bigcap_fset big_seq_fset1.
Qed.

Lemma ( : pointedType) ( : set I)
( : I -> set T) :
countable D -> countable (open_finI_from D f).

Proof.

move=> ?; apply: (card_le_trans (card_image_le _ _)).
exact: fset_subset_countable.
Qed.

Lemma { : choiceType} {} ( : I -> set T) :
setI_closed (open_finI_from D f).

Proof.

move=> A B; case=> N ND <- [M MD <-]; exists (N `|` M)%fset.
by move=> ?; rewrite inE => /orP[/ND | /MD].
by rewrite -bigcap_setU set_fsetU.
Qed.

Lemma { : choiceType} ( : I -> set T) :
open_finI_from D f = \bigcup_ (filterI_iter (f @` D) n).

Proof.

rewrite eqEsubset; split.
  move=> A [N /= + <-]; have /finite_setP[n] := finite_fset N; elim: n N.
    move=> ?; rewrite II0 card_eq0 => /eqP -> _; rewrite bigcap_set0.
    by exists O => //; left.
  move=> n IH N /eq_cardSP[x Ax + ND]; rewrite -set_fsetD1 => Nxn.
  have NxD : {subset (N `\ x)%fset <= D}.
    by move=> ?; rewrite ?inE => /andP [_ /ND /set_mem].
  have [r _ xr] := IH _ Nxn NxD; exists r.+1 => //; exists (f x).
    apply: (@filterI_iter_sub _ _ O) => //; right; exists x => //.
    by rewrite -inE; apply: ND.
  exists (\bigcap_( in [set` (N `\ x)%fset]) f i) => //.
  by rewrite -bigcap_setU1 set_fsetD1 setD1K.
move=> A [n _]; elim: n A.
  (move=> a [-> |[i Di <-]]; [exists fset0 | exists [fset i]%fset]) => //.
  - by rewrite set_fset0 bigcap_set0.
  - by move=> ?; rewrite !inE => /eqP ->.
  - by rewrite set_fset1 bigcap_set1.
by move=> n IH A /= [B snB [C snC <-]]; apply: open_finI_fromI; exact: IH.
Qed.

Lemma { : choiceType} ( : set I) ( : I -> set T) :
filter_from (open_finI_from D f) id = smallest (@Filter T) (f @` D).

Proof.

by rewrite filterI_iter_finI filterI_iterE. Qed.

End filter_supremums.
#[deprecated(since="mathcomp-analysis 1.17.0", use=open_finI_from)]
Notation := open_finI_from (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=open_finI_from_cover)]
Notation := open_finI_from_cover (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=open_finI_from1)]
Notation := open_finI_from1 (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=open_finI_from_countable)]
Notation := open_finI_from_countable (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=open_finI_fromI)]
Notation := open_finI_fromI (only parsing).

Definition ( : choiceType) ( : set I) ( : I -> set T) :=
  forall : {fset I}, {subset D' <= D} ->
  \bigcap_( in [set | i \in D']) f i !=set0.

Lemma ( : choiceType) ( : set I) ( : I -> set T) :
  finI D f -> ProperFilter (filter_from (open_finI_from D f) id).

Proof.

move=> finIf; apply: (filter_from_proper (filter_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.
    by move=> ?; rewrite inE => /orP [/sDA|/sDB].
  rewrite -IfA -IfB predeqE => p; split=> [Ifp|[IfAp IfBp] i].
    by split=> i Di; apply: Ifp; rewrite /= inE Di // orbC.
  by rewrite /= inE => /orP []; [apply: IfAp|apply: IfBp].
- by move=> _ [?? <-]; apply: finIf.
Qed.

Lemma ( : choiceType) ( : set_system T) ( : set_system T)
( : set T -> set T) :
ProperFilter F -> (forall , D A -> F (f A)) -> finI D f.

Proof.

move=> FF sDFf D' sD; apply: (@filter_ex _ F); apply: filter_bigI.
by move=> A /sD; rewrite inE => /sDFf.
Qed.

Lemma ( : set T) :
globally A `#` G = forall , G B -> A `&` B !=set0.

Proof.

rewrite propeqE; split => [/(_ _ _ (fun=> id))//|clA A' B sA].
by move=> /clA; apply: subsetI_neq0.
Qed.

Lemma ( : set T) :
F `#` globally B = forall , F A -> A `&` B !=set0.

Proof.

by rewrite meetsC meets_globallyl; under eq_forall do rewrite setIC.
Qed.

Lemma ( : set_system T) ( : Filter F) : F `#` F = (~ (F set0)).

Proof.

rewrite propeqE; split => [FmF F0|]; first by have [x []] := FmF _ _ F0 F0.
move=> FN0 A B /filterI FAI {}/FAI FAB; apply/set0P/eqP => AB0.
by rewrite AB0 in FAB.
Qed.

Lemma ( : set_system T) ( : ProperFilter F) : F `#` F.

Proof.

by rewrite meetsxx. Qed.

Files

Module mathcomp.classical.filter