From 8148881c9f1bedd2576d2f7e5b4cb2a2a44e1c2b Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Wed, 11 Nov 2020 20:06:23 +0900 Subject: [PATCH] lemmas about closure and connected (#268) - lemmas about `closure` and `connected` - factorized and documented - continuous image of a connected set - Introducing `meets` and factoring several notions - `cluster`, `closure`, `limit_point`, `close_to` and `close` can all be expressed in terms of a set of `meets`. - remove `close_to` Co-authored-by: mkerjean Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 16 +++ theories/boolp.v | 39 +++++ theories/classical_sets.v | 35 +++++ theories/topology.v | 291 ++++++++++++++++++++++++++++++-------- 4 files changed, 323 insertions(+), 58 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 08ccfa56a..f5f17e64c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -64,6 +64,19 @@ + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType` on classical `set`. - file `nngnum.v` + + definition `meets` and its notation `#` + + lemmas `meetsC`, `meets_openr`, `meets_openl`, `meets_globallyl`, + `meets_globallyr `, `meetsxx` and `proper_meetsxx`. +- in `topology.v`: + + definition `limit_point` + + lemmas `subset_limit_point`, `closure_limit_point`, + `closure_subset`, `closureE`, `closureC`, `closure_id` + + lemmas `cluster_nbhs`, `clusterEonbhs`, `closureEcluster` + + definition `separated` + + lemmas `connected0`, `connectedPn`, `connected_continuous_connected` + + lemmas `closureEnbhs`, `closureEonbhs`, `limit_pointEnbhs`, + `limit_pointEonbhs`, `closeEnbhs`, `closeEonbhs`. + ### Changed - in `classical_sets.v`: @@ -115,6 +128,9 @@ - in `discrete.v`: + `existsP` + `existsNP` +- in `topology.v`: + + `close_to` + + `close_cluster`, which is subsumed by `closeEnbhs` ### Infrastructure diff --git a/theories/boolp.v b/theories/boolp.v index 1e6289041..8a164cf14 100644 --- a/theories/boolp.v +++ b/theories/boolp.v @@ -156,16 +156,55 @@ Proof. by rewrite propeqE; split. Qed. Lemma propF (P : Prop) : ~ P -> P = False. Proof. by move=> p; rewrite propeqE; tauto. Qed. +Lemma eq_fun T rT (U V : T -> rT) : + (forall x : T, U x = V x) -> (fun x => U x) = (fun x => V x). +Proof. by move=> /funext->. Qed. + +Lemma eq_fun2 T1 T2 rT (U V : T1 -> T2 -> rT) : + (forall x y, U x y = V x y) -> (fun x y => U x y) = (fun x y => V x y). +Proof. by move=> UV; rewrite funeq2E => x y; rewrite UV. Qed. + +Lemma eq_fun3 T1 T2 T3 rT (U V : T1 -> T2 -> T3 -> rT) : + (forall x y z, U x y z = V x y z) -> + (fun x y z => U x y z) = (fun x y z => V x y z). +Proof. by move=> UV; rewrite funeq3E => x y z; rewrite UV. Qed. + Lemma eq_forall T (U V : T -> Prop) : (forall x : T, U x = V x) -> (forall x, U x) = (forall x, V x). Proof. by move=> e; rewrite propeqE; split=> ??; rewrite (e,=^~e). Qed. +Lemma eq_forall2 T S (U V : forall x : T, S x -> Prop) : + (forall x y, U x y = V x y) -> (forall x y, U x y) = (forall x y, V x y). +Proof. by move=> UV; apply/eq_forall => x; apply/eq_forall. Qed. + +Lemma eq_forall3 T S R (U V : forall (x : T) (y : S x), R x y -> Prop) : + (forall x y z, U x y z = V x y z) -> + (forall x y z, U x y z) = (forall x y z, V x y z). +Proof. by move=> UV; apply/eq_forall2 => x y; apply/eq_forall. Qed. + Lemma eq_exists T (U V : T -> Prop) : (forall x : T, U x = V x) -> (exists x, U x) = (exists x, V x). Proof. by move=> e; rewrite propeqE; split=> - [] x ?; exists x; rewrite (e,=^~e). Qed. +Lemma eq_exists2 T S (U V : forall x : T, S x -> Prop) : + (forall x y, U x y = V x y) -> (exists x y, U x y) = (exists x y, V x y). +Proof. by move=> UV; apply/eq_exists => x; apply/eq_exists. Qed. + +Lemma eq_exists3 T S R (U V : forall (x : T) (y : S x), R x y -> Prop) : + (forall x y z, U x y z = V x y z) -> + (exists x y z, U x y z) = (exists x y z, V x y z). +Proof. by move=> UV; apply/eq_exists2 => x y; apply/eq_exists. Qed. + +Lemma forall_swap T S (U : forall (x : T) (y : S), Prop) : + (forall x y, U x y) = (forall y x, U x y). +Proof. by rewrite propeqE; split. Qed. + +Lemma exists_swap T S (U : forall (x : T) (y : S), Prop) : + (exists x y, U x y) = (exists y x, U x y). +Proof. by rewrite propeqE; split => -[x [y]]; exists y, x. Qed. + Lemma reflect_eq (P : Prop) (b : bool) : reflect P b -> P = b. Proof. by rewrite propeqE; exact: rwP. Qed. diff --git a/theories/classical_sets.v b/theories/classical_sets.v index 568f125ff..a2d962269 100644 --- a/theories/classical_sets.v +++ b/theories/classical_sets.v @@ -66,6 +66,8 @@ Require Import boolp. (* P must be a set on a choiceType. *) (* fun_of_rel f0 f == function that maps x to an element of f x *) (* if there is one, to f0 x otherwise. *) +(* F `#` G <-> intersections beween elements of F an G are *) +(* all non empty. *) (* *) (* * Pointed types: *) (* pointedType == interface type for types equipped with a *) @@ -1168,6 +1170,39 @@ rewrite -Order.TotalTheory.ltNge => kn. by rewrite (Order.POrderTheory.le_trans _ (Em _ Ek)). Qed. +(** ** Intersection of classes of set *) + +Definition meets T (F G : set (set T)) := + forall A B, F A -> G B -> A `&` B !=set0. + +Reserved Notation "A `#` B" + (at level 48, left associativity, format "A `#` B"). + +Notation "F `#` G" := (meets F G) : classical_set_scope. + +Section meets. + +Lemma meetsC T (F G : set (set T)) : F `#` G = G `#` F. +Proof. +gen have sFG : F G / F `#` G -> G `#` F. + by move=> FG B A => /FG; rewrite setIC; apply. +by rewrite propeqE; split; apply: sFG. +Qed. + +Lemma sub_meets T (F F' G G' : set (set T)) : + F `<=` F' -> G `<=` G' -> F' `#` G' -> F `#` G. +Proof. by move=> sF sG FG A B /sF FA /sG GB; apply: (FG A B). Qed. + +Lemma meetsSr T (F G G' : set (set T)) : + G `<=` G' -> F `#` G' -> F `#` G. +Proof. exact: sub_meets. Qed. + +Lemma meetsSl T (G F F' : set (set T)) : + F `<=` F' -> F' `#` G -> F `#` G. +Proof. by move=> /sub_meets; apply. Qed. + +End meets. + Fact set_display : unit. Proof. by []. Qed. Module SetOrder. diff --git a/theories/topology.v b/theories/topology.v index 46baf19ec..dc12f5afb 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -70,16 +70,16 @@ Require Import boolp classical_sets posnum. (* 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 *) +(* 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 *) +(* 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 *) @@ -186,6 +186,7 @@ Require Import boolp classical_sets posnum. (* nbhs' x == set of neighbourhoods of x where x is *) (* excluded. *) (* closure A == closure of the set A. *) +(* limit_point E == the set of limit points of E *) (* closed == set of closed sets. *) (* cluster F == set of cluster points of F. *) (* compact == set of compact sets w.r.t. the filter- *) @@ -195,6 +196,7 @@ Require Import boolp classical_sets posnum. (* cover-based definition of compactness. *) (* connected A <-> the only non empty subset of A which *) (* is both open and closed in A is A. *) +(* separated A B == the two sets A and B are separated *) (* [locally P] := forall a, A a -> G (within A (nbhs x)) *) (* if P is convertible to G (globally A) *) (* *) @@ -557,8 +559,6 @@ Notation "[ 'filteredType' U 'of' T 'for' cT ]" := (@clone U T cT _ idfun) 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) := @@ -2177,6 +2177,42 @@ Proof. by move => FF /cvg_ex [l H]; apply/cvg_ex; exists l; exact: cvg_within_fi Lemma nbhs_nbhs' {T : topologicalType} (x : T) : nbhs' x `=>` nbhs x. Proof. exact: cvg_within. Qed. +(** meets *) + +Lemma meets_openr {T : topologicalType} (F : set (set T)) (x : T) : + F `#` nbhs x = F `#` open_nbhs x. +Proof. +rewrite propeqE; split; [exact/meetsSr/open_nbhs_nbhs|]. +by move=> P A B {}/P P; rewrite nbhsE => -[B' [/P + sB]]; apply: subsetI_neq0. +Qed. + +Lemma meets_openl {T : topologicalType} (F : set (set T)) (x : T) : + nbhs x `#` F = open_nbhs x `#` F. +Proof. by rewrite meetsC meets_openr meetsC. Qed. + +Lemma meets_globallyl T (A : set T) G : + globally A `#` G = forall B, G B -> A `&` B !=set0. +Proof. +rewrite propeqE; split => [/(_ _ _ (fun=> id))//|clA A' B sA]. +by move=> /clA; apply: subsetI_neq0. +Qed. + +Lemma meets_globallyr T F (B : set T) : + F `#` globally B = forall A, F A -> A `&` B !=set0. +Proof. +by rewrite meetsC meets_globallyl; under eq_forall do rewrite setIC. +Qed. + +Lemma meetsxx T (F : set (set T)) (FF : 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 proper_meetsxx T (F : set (set T)) (FF : ProperFilter F) : F `#` F. +Proof. by rewrite meetsxx; apply: filter_not_empty. Qed. + (** ** Closed sets in topological spaces *) Section Closed. @@ -2186,12 +2222,44 @@ Context {T : topologicalType}. Definition closure (A : set T) := [set p : T | forall B, nbhs p B -> A `&` B !=set0]. +Lemma closureEnbhs A : closure A = [set p | globally A `#` nbhs p]. +Proof. by under eq_fun do rewrite meets_globallyl. Qed. + +Lemma closureEonbhs A : closure A = [set p | globally A `#` open_nbhs p]. +Proof. by under eq_fun do rewrite -meets_openr meets_globallyl. Qed. + Lemma subset_closure (A : set T) : A `<=` closure A. 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. +Definition limit_point E := [set t : T | + forall U, nbhs t U -> exists y, [/\ y != t, E y & U y]]. + +Lemma limit_pointEnbhs E : + limit_point E = [set p | globally (E `\ p) `#` nbhs p]. +Proof. +under eq_fun do rewrite meets_globallyl; rewrite funeqE => p /=. +apply/eq_forall2 => x px; apply/eq_exists => y. +by rewrite propeqE; split => [[/eqP ? ?]|[[? /eqP ?]]]; do 2?split. +Qed. + +Lemma limit_pointEonbhs E : + limit_point E = [set p | globally (E `\ p) `#` open_nbhs p]. +Proof. by rewrite limit_pointEnbhs; under eq_fun do rewrite meets_openr. Qed. + +Lemma subset_limit_point E : limit_point E `<=` closure E. +Proof. by move=> t Et U tU; have [p [? ? ?]] := Et _ tU; exists p. Qed. + +Lemma closure_limit_point E : closure E = E `|` limit_point E. +Proof. +rewrite predeqE => t; split => [cEt|]; last first. + by case; [exact: subset_closure|exact: subset_limit_point]. +have [?|Et] := pselect (E t); [by left|right=> U tU; have [p []] := cEt _ tU]. +by exists p; split => //; apply/eqP => pt; apply: Et; rewrite -pt. +Qed. + Definition closed (D : set T) := closure D `<=` D. Lemma closedC (D : set T) : open D -> closed (~` D). @@ -2264,18 +2332,55 @@ Proof. by move=> y fy FDf; apply: (closed_cvg_loc fy); apply: filterE. Qed. +Section closure_lemmas. +Variable T : topologicalType. +Implicit Types E A B U : set T. + +Lemma closure_subset A B : A `<=` B -> closure A `<=` closure B. +Proof. by move=> ? ? CAx ?; move/CAx; exact/subsetI_neq0. Qed. + +Lemma closureE A : closure A = \bigcap_(B in [set B | closed B /\ A `<=` B]) B. +Proof. +rewrite eqEsubset; split=> [x ? B [cB AB]|]; first exact/cB/(closure_subset AB). +by move=> x; apply; split; [exact: closed_closure|exact: subset_closure]. +Qed. + +Lemma closureC E : + ~` closure E = \bigcup_(x in [set U | open U /\ U `<=` ~` E]) x. +Proof. +rewrite closureE bigcapCU setCK eqEsubset; split => t [U [? EU Ut]]. + by exists (~` U) => //; split; [exact: openC|exact: subsetC]. +by rewrite -(setCK E); exists (~` U)=> //; split; [exact:closedC|exact:subsetC]. +Qed. + +Lemma closure_id E : closed E <-> E = closure E. +Proof. +split=> [?|->]; last exact: closed_closure. +rewrite eqEsubset; split => //; exact: subset_closure. +Qed. + +End closure_lemmas. + (** ** Compact sets *) Section Compact. Context {T : topologicalType}. -Definition cluster (F : set (set T)) (p : T) := - forall A B, F A -> nbhs p B -> A `&` B !=set0. +Definition cluster (F : set (set T)) := [set p : T | F `#` nbhs p]. + +Lemma cluster_nbhs t : cluster (nbhs t) t. +Proof. by move=> A B /nbhs_singleton At /nbhs_singleton Bt; exists t. Qed. + +Lemma clusterEonbhs F : cluster F = [set p | F `#` open_nbhs p]. +Proof. by under eq_fun do rewrite -meets_openr. Qed. Lemma clusterE F : cluster F = \bigcap_(A in F) (closure A). Proof. by rewrite predeqE => p; split=> cF ????; apply: cF. Qed. +Lemma closureEcluster E : closure E = cluster (globally E). +Proof. by rewrite closureEnbhs. Qed. + 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. @@ -2652,29 +2757,34 @@ Variable (T : topologicalType). Local Open Scope classical_set_scope. -Definition close_to (x : T) (A : set T) : Prop := - forall N, open_nbhs x N -> N `&` A !=set0. - -Definition close (x y : T) : Prop := - forall M, open_nbhs y M -> close_to x M. +Definition close (x y : T) : Prop := forall M, open_nbhs y M -> closure M x. -Lemma close_refl (t : T) : close t t. -Proof. by move=> M [? ?] N [? ?]; exists t; split. Qed. -Hint Resolve close_refl : core. +Lemma closeEnbhs x : close x = cluster (nbhs x). +Proof. +transitivity (cluster (open_nbhs x)); last first. + by rewrite /cluster; under eq_fun do rewrite -meets_openl. +rewrite clusterEonbhs /close funeqE => y /=; rewrite meetsC /meets. +apply/eq_forall => A; rewrite forall_swap. +by rewrite closureEonbhs meets_globallyl. +Qed. -Lemma close_sym (x y : T) : close x y -> close y x. +Lemma closeEonbhs x : close x = [set y | open_nbhs x `#` open_nbhs y]. Proof. -rewrite /close /close_to => xy N xN M yM. -rewrite setIC; apply xy => //; by case yM. +by rewrite closeEnbhs; under eq_fun do rewrite -meets_openl -meets_openr. Qed. +Lemma close_sym (x y : T) : close x y -> close y x. +Proof. by rewrite !closeEnbhs /cluster meetsC. Qed. + Lemma cvg_close {F} {FF : ProperFilter F} (x y : T) : F --> x -> F --> y -> close x y. Proof. -move=> Fx Fy N yN M xM; near F => z; exists z; split. -- near: z; by apply/Fx; rewrite /filter_of nbhsE; exists M; split. -- near: z; by apply/Fy; rewrite /filter_of nbhsE; exists N; split. -Grab Existential Variables. all: end_near. Qed. +by move=> /sub_meets sx /sx; rewrite closeEnbhs; apply; apply/proper_meetsxx. +Qed. + +Lemma close_refl (x : T) : close x x. +Proof. exact: (@cvg_close (nbhs x)). Qed. +Hint Resolve close_refl : core. Lemma close_cvg (F1 F2 : set (set T)) {FF2 : ProperFilter F2} : F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2). @@ -2725,9 +2835,8 @@ Hypothesis sep : hausdorff T. Lemma closeE (x y : T) : close x y = (x = y). Proof. -rewrite propeqE; split => [cxy|->//]; have [//|xdy] := eqVneq x y. -apply: sep => A B; rewrite !nbhsE => - [oA [xoA oAA]] [oB [xoB oBB]]. -exact: subsetI_neq0 oAA oBB (cxy _ _ _ _). +rewrite propeqE; split; last by move=> ->; exact: close_refl. +by rewrite closeEnbhs; exact: sep. Qed. Lemma close_eq (y x : T) : close x y -> x = y. @@ -2770,12 +2879,92 @@ Qed. End separated_topologicalType. -(* connected sets *) +Section connected_sets. +Variable T : topologicalType. +Implicit Types A B C D : set T. -Definition connected (T : topologicalType) (A : set T) := - forall B : set T, B !=set0 -> (exists2 C, open C & B = A `&` C) -> +Definition connected A := + forall B, B !=set0 -> (exists2 C, open C & B = A `&` C) -> (exists2 C, closed C & B = A `&` C) -> B = A. +Lemma connect0 : connected (@set0 T). +Proof. by move=> ? ? [? ?]; rewrite set0I. Qed. + +Definition separated A B := + (closure A) `&` B = set0 /\ A `&` (closure B) = set0. + +Lemma connectedPn A : ~ connected A <-> + exists E : bool -> set T, [/\ forall b, E b !=set0, + A = E false `|` E true & separated (E false) (E true)]. +Proof. +rewrite -propeqE; apply notLR; rewrite propeqE. +split=> [conE [E [E0 EU [E1 E2]]]|conE B B0 [C oC BAC] [D cD BAD]]. + suff : E true = A. + move/esym/(congr1 (setD^~ (closure (E true)))); rewrite EU setDUl. + have := @subset_closure _ (E true); rewrite -setD_eq0 => ->; rewrite setU0. + by move/setDidPl : E2 => ->; exact/eqP/set0P. + apply: (conE _ (E0 true)). + - exists (~` (closure (E false))); first exact/openC/closed_closure. + rewrite EU setIUl. + have /subsets_disjoint -> := @subset_closure _ (E false); rewrite set0U. + by apply/esym/setIidPl/disjoints_subset; rewrite setIC. + - exists (closure (E true)); first exact: closed_closure. + by rewrite EU setIUl E2 set0U; exact/esym/setIidPl/subset_closure. +apply: contrapT => AF; apply: conE. +exists (fun i => if i is false then A `\` C else A `&` C); split. +- case=> /=; first by rewrite -BAC. + apply/set0P/eqP => /disjoints_subset; rewrite setCK => EC. + by apply: AF; rewrite BAC; exact/setIidPl. +- by rewrite setDE -setIUr setUCl setIT. +- split. + + rewrite setIC; apply/disjoints_subset; rewrite closureC => x [? ?]. + by exists C => //; split=> //; rewrite setDE setCI setCK; right. + + apply/disjoints_subset => y -[Ay Cy]. + rewrite -BAC BAD=> /closureI[_]; rewrite -(proj1 (@closure_id _ _) cD)=> Dy. + by have : B y; [by rewrite BAD; split|rewrite BAC => -[]]. +Qed. + +End connected_sets. + +Lemma connected_continuous_connected (T U : topologicalType) (f : T -> U) A : + connected A -> continuous f -> connected (f @` A). +Proof. +move=> cA cf; apply contrapT => /connectedPn[E [E0 fAE sE]]. +set AfE := fun b => A `&` f @^-1` E b. +suff sAfE : separated (AfE false) (AfE true). + move: cA; apply/connectedPn; exists AfE; split => //. + - move=> b; case: (E0 b) => /= u Ebu. + have [t Et ftu] : (f @` A) u by rewrite fAE; case: b Ebu; [right|left]. + by exists t; split => //; rewrite /preimage ftu. + - by rewrite -setIUr -preimage_setU -fAE; exact/esym/setIidPl/preimage_image. +suff cI0 : forall b, closure (AfE b) `&` AfE (~~ b) = set0. + by rewrite /separated cI0 setIC cI0. +move=> b. +have [fAfE cEIE] : + f @` AfE (~~ b) = E (~~ b) /\ closure (E b) `&` E (~~ b) = set0. + split; last by case: sE => ? ?; case: b => //; rewrite setIC. + rewrite eqEsubset; split. + apply: (subset_trans sub_image_setI). + by apply subIset; right; exact: image_preimage_subset. + move=> u Ebu. + have [t [At ftu]] : exists t, A t /\ f t = u. + suff [t At ftu] : (f @` A) u by exists t. + by rewrite fAE; case: b Ebu; [left|right]. + by exists t => //; split => //; rewrite /preimage ftu. +have ? : f @` closure (AfE b) `<=` closure (E b). + have /(@image_subset _ _ f) : closure (AfE b) `<=` f @^-1` closure (E b). + have /closure_id -> : closed (f @^-1` closure (E b)). + by apply closed_comp => //; exact: closed_closure. + apply: closure_subset. + have /(@preimage_subset _ _ f) A0cA0 := @subset_closure _ (E b). + by apply: subset_trans A0cA0; apply: subIset; right. + by move/subset_trans; apply; exact: image_preimage_subset. +apply/eqP/negPn/negP/set0P => -[t [? ?]]. +have : f @` closure (AfE b) `&` f @` AfE (~~ b) = set0. + by rewrite fAfE; exact: subsetI_eq0 cEIE. +by rewrite predeqE => /(_ (f t)) [fcAfEb] _; apply fcAfEb; split; exists t. +Qed. + (** * Uniform spaces *) Local Notation "B \o A" := @@ -2996,18 +3185,16 @@ move=> entA; split; first exact: open_interior. by apply: nbhs_singleton; apply: nbhs_interior; apply: nbhs_entourage. Qed. -Lemma entourage_close (x y : U) : - close x y = forall A, entourage A -> A (x, y). +Lemma entourage_close (x y : U) : close x y = forall A, entourage A -> A (x, y). Proof. rewrite propeqE; split=> [cxy A entA|cxy]. - have /entourage_split_ent entsA := entA. - have [z [/interior_subset zx /interior_subset /= zy]] := - cxy _ (open_nbhs_entourage _ (entourage_inv entsA)) - _ (open_nbhs_entourage _ entsA). + have /entourage_split_ent entsA := entA; rewrite closeEnbhs in cxy. + have yl := nbhs_entourage _ (entourage_inv entsA). + have yr := nbhs_entourage _ entsA. + have [z [zx zy]] := cxy _ _ (yr x) (yl y). exact: (entourage_split z). -move=> A /open_nbhs_nbhs/nbhsP[E1 entE1 sE1A]. -move=> B /open_nbhs_nbhs/nbhsP[E2 entE2 sE2B]. -by exists y; split; [apply/sE2B; apply: cxy|apply/sE1A; apply: entourage_refl]. +rewrite closeEnbhs => A B /nbhsP[E1 entE1 sE1A] /nbhsP[E2 entE2 sE2B]. +by exists y; split;[apply: sE1A; apply: cxy|apply: sE2B; apply: entourage_refl]. Qed. Lemma close_trans (y x z : U) : close x y -> close y z -> close x z. @@ -3032,19 +3219,6 @@ move=> FF; split=> [Fl|[cvF]Cl]. by apply: cvg_trans (close_cvgxx Cl). Qed. -Lemma close_cluster (x y : U) : close x y = cluster (nbhs x) y. -Proof. -rewrite propeqE; split => xy. -- move=> A B xA; rewrite -nbhs_entourageE => -[E entE sEB]. - exists x; split; first exact: nbhs_singleton. - by apply/sEB; move/close_sym: xy; rewrite entourage_close; apply. -- rewrite entourage_close => A entA. - have /entourage_split_ent entsA := entA. - have [z [/= zx zy]] := - xy _ _ (nbhs_entourage _ entsA) (nbhs_entourage _ (entourage_inv entsA)). - exact: (entourage_split z). -Qed. - End uniform_closeness. Definition unif_continuous (U V : uniformType) (f : U -> V) := @@ -3578,12 +3752,13 @@ Lemma ball_close (x y : M) : close x y = forall eps : {posnum R}, ball x eps%:num y. Proof. rewrite propeqE; split => [cxy eps|cxy]. - have [z [zx zy]] := cxy _ (open_nbhs_ball _ (eps%:num/2)%:pos) - _ (open_nbhs_ball _ (eps%:num/2)%:pos). + have := cxy _ (open_nbhs_ball _ (eps%:num/2)%:pos). + rewrite closureEonbhs meetsC meets_globallyr. + move/(_ _ (open_nbhs_ball _ (eps%:num/2)%:pos)) => [z [zx zy]]. by apply: (@ball_splitl z); apply: interior_subset. -move=> B /open_nbhs_nbhs/nbhs_ballP[_/posnumP[e2 e2B]]. -move=> A /open_nbhs_nbhs/nbhs_ballP[_/posnumP[e1 e1A]]. -by exists y; split; [apply/e1A|apply/e2B/ballxx]. +rewrite closeEnbhs => B A /nbhs_ballP[_/posnumP[e2 e2B]] + /nbhs_ballP[_/posnumP[e1 e1A]]. +by exists y; split; [apply/e2B|apply/e1A; exact: ballxx]. Qed. End pseudoMetricType_numFieldType.