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 <[email protected]>
Co-authored-by: Cyril Cohen <[email protected]>

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
 

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.
 

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.