Module mathcomp.analysis.topology_theory.supremum_topology
From HB Require Import structures.From mathcomp Require Import boot order algebra finmap all_classical.
From mathcomp Require Import topology_structure uniform_structure.
# Supremum topology
```
sup_topology Tc == supremum topology of the family of
topologicalType structures Tc on T
sup_ent E == the entourages of the supremum
```
`sup_topology` is equipped with the `Uniform` structure
Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Definition
sup_topology
Source code
{ : Type} { : Type}cauchy : forall {T : uniformType}, set_system T -> Prop cauchy is not universe polymorphic Arguments cauchy {T} F cauchy is transparent Expands to: Constant mathcomp.analysis.topology_theory.uniform_structure.cauchy Declared in library mathcomp.analysis.topology_theory.uniform_structure, line 337, characters 11-17
Source code
( : I -> Topological T) : Type := T.
Section Sup_Topology.
Variable ( : choiceType) ( : Type) ( : I -> Topological T).
Local Notation := (sup_topology Tc).
Let := fun => Topological.Pack (Tc i).
Definition
sup_subbase
Source code
:= \bigcup_ (@open (TS i) : set_system T).Source code
.
instance
Source code
Source code
Definition
Source code
Source code
Choice
Source code
.on S.Source code
.
instance
Source code
Source code
Definition
Source code
Source code
isSubBaseTopological
Source code
.Build S sup_subbase id.Source code
Lemma
cvg_sup
Source code
( : set_system T) ( : T) :Source code
Filter F -> F --> (t : S) <-> forall , 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 inE inE => /eqP->; exists i.
by rewrite predeqE=> ?; split=> [|??]; [apply|]; rewrite /= inE // =>/eqP->.
move=> A /=; rewrite (@nbhsE S).
move=> [_ [[B sB <-] [C BC Ct] sUBA]].
rewrite nbhs_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 inE => - [i _]; rewrite openE => Eop.
by apply: (cvFt i); apply: Eop; move: Ct; rewrite -IDeC => /(_ _ DE).
Qed.
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 inE inE => /eqP->; exists i.
by rewrite predeqE=> ?; split=> [|??]; [apply|]; rewrite /= inE // =>/eqP->.
move=> A /=; rewrite (@nbhsE S).
move=> [_ [[B sB <-] [C BC Ct] sUBA]].
rewrite nbhs_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 inE => - [i _]; rewrite openE => Eop.
by apply: (cvFt i); apply: Eop; move: Ct; rewrite -IDeC => /(_ _ DE).
Qed.
End Sup_Topology.
.
instance
Source code
Source code
Definition
Source code
(Source code
Type
Source code
) (Source code
pointedType
Source code
) (f : I -> Topological T) :=Source code
Pointed.on (sup_topology f).
Section sup_uniform.
Local Open Scope relation_scope.
Context { : choiceType} { : Type} ( : Ii -> Uniform T).
Let : choiceType := {classic Ii}.
Let := fun => Uniform.Pack (Tc i).
Notation := (sup_topology Tc).
Let
ent_of
Source code
( : I * set (T * T)) := `[< @entourage (TS p.1) p.2 >].Source code
Let
IEntType
Source code
:= { : (I * set (T * T)) | ent_of p}.Source code
Let
IEnt
Source code
: choiceType := IEntType.Source code
Local Lemma
IEnt_pointT
Source code
( : I) : ent_of (i, setT).Source code
Proof.
Definition
sup_ent
Source code
: set_system (T * T) :=Source code
filter_from (open_finI_from [set: IEnt] (fun => (projT1 p).2)) id.
Ltac IEntP := move=> [[ /= + + /[dup] /asboolP]].
Local Lemma
sup_ent_filter
Source code
: Filter sup_ent.Source code
Proof.
case: (pselect (exists :T, True)).
case => p _; apply: finI_filter; move=> J JsubEnt /=; exists (p, p).
by IEntP => i b /= /entourage_refl ? ? _.
move=> empT.
have TT0 ( : set (T*T)) : E = set0.
rewrite eqEsubset; split => //=; case=> t ? _; move: empT.
by apply: Logic.absurd; exists t.
have ent0 : sup_ent set0.
rewrite -(TT0 setT); exists set0 => //=; exists fset0 => //=.
split.
- rewrite (TT0 setT); exact: ent0.
- by move => P Q ? ?; rewrite (TT0 (P `&` Q)).
- by move=> P Q _ _; rewrite (TT0 Q).
Qed.
case => p _; apply: finI_filter; move=> J JsubEnt /=; exists (p, p).
by IEntP => i b /= /entourage_refl ? ? _.
move=> empT.
have TT0 ( : set (T*T)) : E = set0.
rewrite eqEsubset; split => //=; case=> t ? _; move: empT.
by apply: Logic.absurd; exists t.
have ent0 : sup_ent set0.
rewrite -(TT0 setT); exists set0 => //=; exists fset0 => //=.
split.
- rewrite (TT0 setT); exact: ent0.
- by move => P Q ? ?; rewrite (TT0 (P `&` Q)).
- by move=> P Q _ _; rewrite (TT0 Q).
Qed.
Local Lemma
sup_ent_refl
Source code
: sup_ent A -> diagonal `<=` A.Source code
Proof.
Local Lemma
sup_ent_inv
Source code
: sup_ent A -> sup_ent A^-1.Source code
Proof.
move=> [B [F ? FB] BA]; exists B^-1; last by move=> ?; exact: BA.
have inv : forall : IEnt, ent_of ((projT1 ie).1, (projT1 ie).2^-1).
by IEntP=> ?? /entourage_inv ??; exact/asboolP.
exists [fset (fun => @exist (I * set (T * T)) _ _ (inv x)) w | in F]%fset.
by move=> ? /imfsetP; IEntP => ? ? ? ? ->; exact: in_setT.
rewrite -FB eqEsubset; split; case=> x y + ie.
by move=> /(_ (exist ent_of _ (inv ie))) + ?; apply; apply/imfsetP; exists ie.
by move=> + /imfsetP [v vW ->]; exact.
Qed.
have inv : forall : IEnt, ent_of ((projT1 ie).1, (projT1 ie).2^-1).
by IEntP=> ?? /entourage_inv ??; exact/asboolP.
exists [fset (fun => @exist (I * set (T * T)) _ _ (inv x)) w | in F]%fset.
by move=> ? /imfsetP; IEntP => ? ? ? ? ->; exact: in_setT.
rewrite -FB eqEsubset; split; case=> x y + ie.
by move=> /(_ (exist ent_of _ (inv ie))) + ?; apply; apply/imfsetP; exists ie.
by move=> + /imfsetP [v vW ->]; exact.
Qed.
Local Lemma
sup_ent_split
Source code
: sup_ent A -> exists2 , sup_ent B & B \; B `<=` A.Source code
Proof.
have spt : (forall : IEnt, ent_of ((projT1 ie).1,
(@split_ent (TS (projT1 ie).1) (projT1 ie).2))).
by case=> [[/= ? ?] /asboolP/entourage_split_ent ?]; exact/asboolP.
pose g : (IEnt -> IEnt) := fun => exist ent_of _ (spt x).
case => W [F _ <-] sA; exists (\bigcap_( in [set` F]) (projT1 (g x)).2).
exists (\bigcap_( in [set`F]) (projT1 (g ie)).2) => //.
exists [fset (g ie) | in F]%fset; first by move=> /= ??; exact: in_setT.
rewrite eqEsubset; split; case=> x y Igxy ie.
by move => ?; apply/(Igxy (g ie))/imfsetP; exists ie.
by move=> /imfsetP [?? ->]; exact: Igxy.
case => ?? [z Fxz Fzy]; apply: sA; IEntP=> i e ? ? eF.
apply: ((@entourage_split (TS i)) z) => //.
exact: (Fxz _ eF).
exact: (Fzy _ eF).
Qed.
(@split_ent (TS (projT1 ie).1) (projT1 ie).2))).
by case=> [[/= ? ?] /asboolP/entourage_split_ent ?]; exact/asboolP.
pose g : (IEnt -> IEnt) := fun => exist ent_of _ (spt x).
case => W [F _ <-] sA; exists (\bigcap_( in [set` F]) (projT1 (g x)).2).
exists (\bigcap_( in [set`F]) (projT1 (g ie)).2) => //.
exists [fset (g ie) | in F]%fset; first by move=> /= ??; exact: in_setT.
rewrite eqEsubset; split; case=> x y Igxy ie.
by move => ?; apply/(Igxy (g ie))/imfsetP; exists ie.
by move=> /imfsetP [?? ->]; exact: Igxy.
case => ?? [z Fxz Fzy]; apply: sA; IEntP=> i e ? ? eF.
apply: ((@entourage_split (TS i)) z) => //.
exact: (Fxz _ eF).
exact: (Fzy _ eF).
Qed.
Local Lemma
sup_ent_nbhs
Source code
: @nbhs Tt Tt = nbhs_ sup_ent.Source code
Proof.
rewrite predeq2E => x V; split.
move=> [/= X [[/= B + <-] [W BW Wx BV]]] => /(_ W BW) [] /=.
move=> F Fsup Weq; move: Weq Wx BW => <- Fx BF.
case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]].
suff -> : V = setT by exists setT; apply: filterT; exact: sup_ent_filter.
rewrite -subTset => ??; apply: BV; exists (\bigcap_( in [set` F]) i) => //.
by move=> w /Fsup/set_mem; rewrite /sup_subbase I0 bigcup_set0.
have f : forall , { : IEnt | w \in F -> xsection ((projT1 p).2) x `<=` w}.
move=> /= v; apply: cid; case (pselect (v \in F)); first last.
by move=> ?; exists (exist ent_of _ (IEnt_pointT i0)).
move=> /[dup] /Fx vx /Fsup/set_mem [i _]; rewrite openE => /(_ x vx).
by move=> /(@nbhsP (TS i)) [w /asboolP ent ?]; exists (exist _ (i, w) ent).
exists (\bigcap_( in [set` F]) (projT1 (projT1 (f w))).2); first last.
move=> v /= /xsectionP Fgw; apply: BV; exists (\bigcap_( in [set` F]) i) => //.
by move=> w /[dup] ? /Fgw /= /mem_set/(projT2 (f w)); exact.
exists (\bigcap_( in [set` F]) (projT1 (projT1 (f w))).2) => //.
exists [fset (fun => projT1 (f i)) w | in F]%fset.
by move=> u ?; exact: in_setT.
rewrite eqEsubset; split => y + z.
by move=>/(_ (projT1 (f z))) => + ?; apply; apply/imfsetP; exists z.
by move=> Fgy /imfsetP [/= u uF ->]; exact: Fgy.
case=> E [D [/= F FsubEnt <-] FsubE EsubV].
have F_nbhs_x : Filter (nbhs x) by typeclasses eauto.
apply: (filterS EsubV).
pose f : IEnt -> set T := fun =>
@interior (TS (projT1 w).1) (xsection (projT1 w).2 x).
exists (\bigcap_( in [set` F]) f w); repeat split.
- exists [set \bigcap_( in [set` F]) f w]; last by rewrite bigcup_set1.
move=> ? ->; exists [fset f w | in F]%fset.
move=> /= ? /imfsetP [[[/= i w /[dup] /asboolP entw ? Fiw ->]]].
by apply/mem_set; rewrite /f /=; exists i => //; exact: open_interior.
by rewrite set_imfset bigcap_image //=.
- by IEntP=> ? ? /open_nbhs_entourage entw ??; apply entw.
- move=> t /= Ifwt.
by apply/mem_set/FsubE => it /Ifwt/interior_subset => /set_mem.
Qed.
move=> [/= X [[/= B + <-] [W BW Wx BV]]] => /(_ W BW) [] /=.
move=> F Fsup Weq; move: Weq Wx BW => <- Fx BF.
case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]].
suff -> : V = setT by exists setT; apply: filterT; exact: sup_ent_filter.
rewrite -subTset => ??; apply: BV; exists (\bigcap_( in [set` F]) i) => //.
by move=> w /Fsup/set_mem; rewrite /sup_subbase I0 bigcup_set0.
have f : forall , { : IEnt | w \in F -> xsection ((projT1 p).2) x `<=` w}.
move=> /= v; apply: cid; case (pselect (v \in F)); first last.
by move=> ?; exists (exist ent_of _ (IEnt_pointT i0)).
move=> /[dup] /Fx vx /Fsup/set_mem [i _]; rewrite openE => /(_ x vx).
by move=> /(@nbhsP (TS i)) [w /asboolP ent ?]; exists (exist _ (i, w) ent).
exists (\bigcap_( in [set` F]) (projT1 (projT1 (f w))).2); first last.
move=> v /= /xsectionP Fgw; apply: BV; exists (\bigcap_( in [set` F]) i) => //.
by move=> w /[dup] ? /Fgw /= /mem_set/(projT2 (f w)); exact.
exists (\bigcap_( in [set` F]) (projT1 (projT1 (f w))).2) => //.
exists [fset (fun => projT1 (f i)) w | in F]%fset.
by move=> u ?; exact: in_setT.
rewrite eqEsubset; split => y + z.
by move=>/(_ (projT1 (f z))) => + ?; apply; apply/imfsetP; exists z.
by move=> Fgy /imfsetP [/= u uF ->]; exact: Fgy.
case=> E [D [/= F FsubEnt <-] FsubE EsubV].
have F_nbhs_x : Filter (nbhs x) by typeclasses eauto.
apply: (filterS EsubV).
pose f : IEnt -> set T := fun =>
@interior (TS (projT1 w).1) (xsection (projT1 w).2 x).
exists (\bigcap_( in [set` F]) f w); repeat split.
- exists [set \bigcap_( in [set` F]) f w]; last by rewrite bigcup_set1.
move=> ? ->; exists [fset f w | in F]%fset.
move=> /= ? /imfsetP [[[/= i w /[dup] /asboolP entw ? Fiw ->]]].
by apply/mem_set; rewrite /f /=; exists i => //; exact: open_interior.
by rewrite set_imfset bigcap_image //=.
- by IEntP=> ? ? /open_nbhs_entourage entw ??; apply entw.
- move=> t /= Ifwt.
by apply/mem_set/FsubE => it /Ifwt/interior_subset => /set_mem.
Qed.
.
instance
Source code
Source code
Definition
Source code
Source code
@Nbhs_isUniform
Source code
.Build Tt sup_entSource code
sup_ent_filter sup_ent_refl sup_ent_inv sup_ent_split sup_ent_nbhs.
Lemma
countable_sup_ent
Source code
:Source code
countable [set: Ii] -> (forall , countable_uniformity (TS n)) ->
countable_uniformity Tt.
Proof.
move=> Icnt countable_ent; pose f := cid (countable_ent n).
pose g ( : Ii) : set_system (T * T) := projT1 (f n).
have [I0 | /set0P [i0 _]] := eqVneq [set: I] set0.
exists [set setT]; split; [exact: countable1|move=> A ->; exact: entourageT|].
move=> P [w [A _]] <- subP; exists setT => //.
apply: subset_trans subP; apply: sub_bigcap => i _ ? _.
by suff : [set: I] (projT1 i).1 by rewrite I0.
exists (open_finI_from (\bigcup_ g n) id); split.
- apply/open_finI_from_countable/bigcup_countable => // i _.
by case: (projT2 (f i)).
- move=> E [A AsubGn AE]; exists E => //.
have h ( : set (T * T)) : { : IEnt | w \in A -> w = (projT1 p).2 }.
apply: cid; have [|] := boolP (w \in A); last first.
by exists (exist ent_of _ (IEnt_pointT i0)).
move=> /[dup] /AsubGn /set_mem [n _ gnw] wA.
suff ent : ent_of (n, w) by exists (exist ent_of (n, w) ent).
by apply/asboolP; have [_ + _] := projT2 (f n); exact.
exists [fset sval (h w) | in A]%fset; first by move=> ?; exact: in_setT.
rewrite -AE; rewrite eqEsubset; split => t Ia.
by move=> w Aw; rewrite (svalP (h w) Aw); apply/Ia/imfsetP; exists w.
case=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia.
by rewrite (_ : w = x) // (svalP (h x) xA) -M.
- move=> E [w] [ A _ wIA wsubE].
have ent_Ip ( : IEnt) : @entourage (TS (projT1 i).1) (projT1 i).2.
by apply/asboolP; exact: (projT2 i).
pose h ( : IEnt) : { : set (T * T) | _} := cid2 (and3_rec
(fun _ _ => P) (projT2 (f (projT1 i).1)) (projT1 i).2 (ent_Ip i)).
have ehi ( : IEnt) : ent_of ((projT1 i).1, projT1 (h i)).
apply/asboolP => /=; have [] := projT2 (h i).
by have [_ + _ ? ?] := projT2 (f (projT1 i).1); exact.
pose AH := [fset projT1 (h w) | in A]%fset.
exists (\bigcap_( in [set` AH]) i).
exists AH => // p /imfsetP [i iA ->]; rewrite inE //.
by exists (projT1 i).1 => //; have [] := projT2 (h i).
apply: subset_trans wsubE; rewrite -wIA => ? It i ?.
by have [?] := projT2 (h i); apply; apply: It; apply/imfsetP; exists i.
Qed.
pose g ( : Ii) : set_system (T * T) := projT1 (f n).
have [I0 | /set0P [i0 _]] := eqVneq [set: I] set0.
exists [set setT]; split; [exact: countable1|move=> A ->; exact: entourageT|].
move=> P [w [A _]] <- subP; exists setT => //.
apply: subset_trans subP; apply: sub_bigcap => i _ ? _.
by suff : [set: I] (projT1 i).1 by rewrite I0.
exists (open_finI_from (\bigcup_ g n) id); split.
- apply/open_finI_from_countable/bigcup_countable => // i _.
by case: (projT2 (f i)).
- move=> E [A AsubGn AE]; exists E => //.
have h ( : set (T * T)) : { : IEnt | w \in A -> w = (projT1 p).2 }.
apply: cid; have [|] := boolP (w \in A); last first.
by exists (exist ent_of _ (IEnt_pointT i0)).
move=> /[dup] /AsubGn /set_mem [n _ gnw] wA.
suff ent : ent_of (n, w) by exists (exist ent_of (n, w) ent).
by apply/asboolP; have [_ + _] := projT2 (f n); exact.
exists [fset sval (h w) | in A]%fset; first by move=> ?; exact: in_setT.
rewrite -AE; rewrite eqEsubset; split => t Ia.
by move=> w Aw; rewrite (svalP (h w) Aw); apply/Ia/imfsetP; exists w.
case=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia.
by rewrite (_ : w = x) // (svalP (h x) xA) -M.
- move=> E [w] [ A _ wIA wsubE].
have ent_Ip ( : IEnt) : @entourage (TS (projT1 i).1) (projT1 i).2.
by apply/asboolP; exact: (projT2 i).
pose h ( : IEnt) : { : set (T * T) | _} := cid2 (and3_rec
(fun _ _ => P) (projT2 (f (projT1 i).1)) (projT1 i).2 (ent_Ip i)).
have ehi ( : IEnt) : ent_of ((projT1 i).1, projT1 (h i)).
apply/asboolP => /=; have [] := projT2 (h i).
by have [_ + _ ? ?] := projT2 (f (projT1 i).1); exact.
pose AH := [fset projT1 (h w) | in A]%fset.
exists (\bigcap_( in [set` AH]) i).
exists AH => // p /imfsetP [i iA ->]; rewrite inE //.
by exists (projT1 i).1 => //; have [] := projT2 (h i).
apply: subset_trans wsubE; rewrite -wIA => ? It i ?.
by have [?] := projT2 (h i); apply; apply: It; apply/imfsetP; exists i.
Qed.
End sup_uniform.