Redefine Subnet

theories/Topology/Compactness.v

@@ -299,7 +299,7 @@ Qed.
 
 Lemma compact_impl_net_cluster_point:
   forall X:TopologicalSpace, compact X ->
-    forall (I:DirectedSet) (x:Net I X), inhabited (DS_set I) ->
+    forall (I:DirectedSet) (x:Net I X), inhabited I ->
     exists x0:X, net_cluster_point x x0.
 Proof.
 intros.
@@ -311,7 +311,7 @@ apply H1.
 Qed.
 
 Lemma net_cluster_point_impl_compact: forall X:TopologicalSpace,
-  (forall (I:DirectedSet) (x:Net I X), inhabited (DS_set I) ->
+  (forall (I:DirectedSet) (x:Net I X), inhabited I ->
     exists x0:X, net_cluster_point x x0) ->
   compact X.
 Proof.
@@ -357,13 +357,13 @@ apply Extensionality_Ensembles; split; red; intros.
   apply closure_inflationary. assumption.
 }
 destruct (net_limits_determine_topology _ _ H2) as [I0 [y []]].
-pose (yS (i:DS_set I0) := exist (fun x:X => In S x) (y i) (H3 i)).
+pose (yS (i:I0) := exist (fun x:X => In S x) (y i) (H3 i)).
 assert (inhabited (SubspaceTopology S)).
 { destruct H1.
   constructor.
   now exists x0.
 }
-assert (inhabited (DS_set I0)) as HinhI0.
+assert (inhabited I0) as HinhI0.
 { red in H4.
   destruct (H4 Full_set) as [i0]; auto with topology.
   constructor.
@@ -378,16 +378,18 @@ apply net_cluster_point_impl_subnet_converges in H6.
   - constructor.
   - now constructor.
 }
-destruct H6 as [J [y' []]].
-destruct H6.
-assert (net_limit (fun j:DS_set J => y (h j)) x0).
+destruct H6 as [J [y' [HySy' Hy']]].
+destruct HySy' as [h [Hh0 [Hh1 Hhy']]].
+assert (net_limit (fun j:J => y (h j)) x0).
 { apply continuous_func_preserves_net_limits with
-  (f:=subspace_inc S) (Y:=X) in H7.
-  - assumption.
+  (f:=subspace_inc S) (Y:=X) in Hy'.
+  - cbn in Hy'.
+    eapply net_limit_compat; eauto.
+    intros ?; cbn. rewrite Hhy'. reflexivity.
   - apply continuous_func_continuous_everywhere, subspace_inc_continuous. }
-assert (net_limit (fun j:DS_set J => y (h j)) x).
+assert (net_limit (fun j:J => y (h j)) x).
 { apply subnet_limit with I0 y; trivial.
-  now constructor. }
+  exists h. now constructor. }
 assert (x = x0).
 { eapply Hausdorff_impl_net_limit_unique; eassumption. }
 now subst.
@@ -441,7 +443,7 @@ intros.
 apply net_cluster_point_impl_compact.
 intros.
 destruct (compact_impl_net_cluster_point _ H
-  _ (fun i:DS_set I => subspace_inc _ (x i))) as [x0]; trivial.
+  _ (fun i:I => subspace_inc _ (x i))) as [x0]; trivial.
 assert (In S x0).
 { rewrite <- (closure_fixes_closed S); trivial.
   eapply net_cluster_point_in_closure;

theories/Topology/Completeness.v

@@ -14,7 +14,7 @@
 Definition complete : Prop :=
   forall x:nat -> X, cauchy x ->
     exists x0 : X, forall eps:R,
-      eps > 0 -> for large i:DS_set nat_DS,
+      eps > 0 -> for large i:nat_DS,
       d x0 (x i) < eps.
 
 Lemma cauchy_impl_bounded (x : nat -> X) :
@@ -54,7 +54,7 @@
 inversion Hy; subst; clear Hy.
 rename x0 into n. clear Hx d_metric.
 constructor.
 destruct (le_or_lt N n).
 - apply Rlt_le_trans with 1; auto.
   unfold Rmax.
   destruct (Rle_dec _ _); lra.

theories/Topology/FiltersAndNets.v

@@ -7,10 +7,10 @@ Section net_tail_filter.
 Variable X:TopologicalSpace.
 Variable J:DirectedSet.
 Variable x:Net J X.
-Hypothesis J_nonempty: inhabited (DS_set J).
+Hypothesis J_nonempty: inhabited J.
 
-Definition net_tail (j:DS_set J) :=
-  Im [ i:DS_set J | DS_ord j i ] x.
+Definition net_tail (j:J) :=
+  Im [ i:J | DS_ord j i ] x.
 
 Definition tail_filter_basis : Family (point_set X) :=
   Im Full_set net_tail.

theories/Topology/MetricSpaces.v

@@ -287,7 +287,7 @@
 Lemma metric_space_net_limit: forall (X:TopologicalSpace)
   (d:X -> X -> R), metrizes X d ->
   forall (I:DirectedSet) (x:Net I X) (x0:X),
-  (forall eps:R, eps > 0 -> for large i:DS_set I, d x0 (x i) < eps) ->
+  (forall eps:R, eps > 0 -> for large i:I, d x0 (x i) < eps) ->
   net_limit x x0.
 Proof.
 intros.
@@ -306,7 +306,7 @@
   (d:X -> X -> R), metrizes X d ->
   forall (I:DirectedSet) (x:Net I X) (x0:X),
     net_limit x x0 -> forall eps:R, eps > 0 ->
-                         for large i:DS_set I, d x0 (x i) < eps.
+                         for large i:I, d x0 (x i) < eps.
 Proof.
 intros.
 pose (U:=open_ball d x0 eps).
@@ -324,7 +324,7 @@
   (d:X -> X -> R), metrizes X d ->
   forall (I:DirectedSet) (x:Net I X) (x0:X),
   (forall eps:R, eps > 0 ->
-     exists arbitrarily large i:DS_set I, d x0 (x i) < eps) ->
+     exists arbitrarily large i:I, d x0 (x i) < eps) ->
   net_cluster_point x x0.
 Proof.
 intros.
@@ -344,7 +344,7 @@
   (d:X -> X -> R), metrizes X d ->
   forall (I:DirectedSet) (x:Net I X) (x0:X),
     net_cluster_point x x0 -> forall eps:R, eps > 0 ->
-                exists arbitrarily large i:DS_set I, d x0 (x i) < eps.
+                exists arbitrarily large i:I, d x0 (x i) < eps.
 Proof.
 intros.
 pose (U:=open_ball d x0 eps).
@@ -678,7 +678,7 @@
     2: { contradiction. }
     destruct H4. destruct H4, H5.
     assert (d x x0 + d x0 y < d x y).
     { rewrite double_var.
       apply Rplus_lt_compat; try assumption.
       rewrite metric_sym; assumption.
     }

theories/Topology/Nets.v

@@ -4,28 +4,72 @@ From Topology Require Export TopologicalSpaces InteriorsClosures Continuity.
 Set Asymmetric Patterns.
 
 Definition Net (I : DirectedSet) (X : Type) : Type :=
-  DS_set I -> X.
+  I -> X.
+
+Definition Subnet {I : DirectedSet} {X : Type}
+  (x : Net I X) {J : DirectedSet} (y : Net J X) : Prop :=
+  exists (h : J -> I),
+    (* [h] is monotonous *)
+    (forall j1 j2 : J,
+        DS_ord j1 j2 -> DS_ord (h j1) (h j2)) /\
+    (exists arbitrarily large i : I,
+      exists j : J, h j = i) /\
+    (* [y] is [x ∘ h] *)
+    (forall j : J,
+        y j = x (h j)).
+
+Lemma Subnet_refl {I : DirectedSet} {X : Type} (x : Net I X) :
+  Subnet x x.
+Proof.
+  exists id. split; [|split].
+  - tauto.
+  - intros i. exists i. split.
+    + apply I.
+    + exists i; reflexivity.
+  - reflexivity.
+Qed.
 
-Inductive Subnet {I : DirectedSet} {X : Type}
-  (x : Net I X) {J : DirectedSet} : Net J X -> Prop :=
-| intro_subnet: forall h:DS_set J -> DS_set I,
-    (forall j1 j2:DS_set J,
-        DS_ord j1 j2 -> DS_ord (h j1) (h j2)) ->
-    (exists arbitrarily large i:DS_set I,
-      exists j:DS_set J, h j = i) ->
-    Subnet x (fun j:DS_set J => x (h j)).
+Lemma Subnet_trans {I J K : DirectedSet} {X : Type}
+  (x : Net I X) (y : Net J X) (z : Net K X) :
+  Subnet x y -> Subnet y z -> Subnet x z.
+Proof.
+  intros [f [Hf1 [Hf2 Hf3]]]
+         [g [Hg1 [Hg2 Hg3]]].
+  exists (compose f g). split; [|split].
+  - intros j1 j2 Hjj. apply Hf1, Hg1, Hjj.
+  - intros i.
+    specialize (Hf2 i) as [j0 [Hij [j Hj]]].
+    subst j0.
+    specialize (Hg2 j) as [k0 [Hjk [k Hk]]].
+    subst k0.
+    exists (f (g k)). split.
+    + apply preord_trans with (f j); auto. apply I.
+    + exists k. reflexivity.
+  - intros k. rewrite Hg3, Hf3. reflexivity.
+Qed.
 
 Section Net.
 Variable I:DirectedSet.
 Variable X:TopologicalSpace.
 
 Definition net_limit (x:Net I X) (x0:X) : Prop :=
   forall U:Ensemble X, open U -> In U x0 ->
-  for large i:DS_set I, In U (x i).
+  for large i:I, In U (x i).
 
 Definition net_cluster_point (x:Net I X) (x0:X) : Prop :=
   forall U:Ensemble X, open U -> In U x0 ->
-  exists arbitrarily large i:DS_set I, In U (x i).
+  exists arbitrarily large i:I, In U (x i).
+
+Lemma net_limit_compat (x1 x2 : Net I X) (x : X) :
+  (forall i : I, x1 i = x2 i) ->
+  net_limit x1 x -> net_limit x2 x.
+Proof.
+  intros Hxx Hx1.
+  intros U HU HUx.
+  specialize (Hx1 U HU HUx) as [i Hi].
+  exists i. intros i0 Hii.
+  rewrite <- Hxx. apply Hi; assumption.
+Qed.
 
 Lemma net_limit_is_cluster_point: forall (x:Net I X) (x0:X),
   net_limit x x0 -> net_cluster_point x x0.
@@ -43,7 +87,7 @@ Qed.
 
 Lemma net_limit_in_closure: forall (S:Ensemble X)
   (x:Net I X) (x0:X),
-  (exists arbitrarily large i:DS_set I, In S (x i)) ->
+  (exists arbitrarily large i:I, In S (x i)) ->
   net_limit x x0 -> In (closure S) x0.
 Proof.
 intros.
@@ -61,7 +105,7 @@ Qed.
 
 Lemma net_cluster_point_in_closure: forall (S:Ensemble X)
   (x:Net I X) (x0:X),
-  (for large i:DS_set I, In S (x i)) ->
+  (for large i:I, In S (x i)) ->
   net_cluster_point x x0 -> In (closure S) x0.
 Proof.
 intros.
@@ -148,7 +192,7 @@ Lemma net_limits_determine_topology:
   forall {X:TopologicalSpace} (S:Ensemble X)
   (x0:X), In (closure S) x0 ->
   exists I:DirectedSet, exists x:Net I X,
-  (forall i:DS_set I, In S (x i)) /\ net_limit x x0.
+  (forall i:I, In S (x i)) /\ net_limit x x0.
 Proof.
 intros.
 assert (forall U:Ensemble X, open U -> In U x0 ->
@@ -229,7 +273,7 @@ Variable f:X -> Y.
 Lemma continuous_func_preserves_net_limits:
   forall {I:DirectedSet} (x:Net I X) (x0:X),
     net_limit x x0 -> continuous_at f x0 ->
-    net_limit (fun i:DS_set I => f (x i)) (f x0).
+    net_limit (fun i:I => f (x i)) (f x0).
 Proof.
 intros.
 red. intros V ? ?.
@@ -239,7 +283,7 @@ assert (neighborhood V (f x0)).
 destruct (H0 V H3) as [U [? ?]].
 destruct H4.
 pose proof (H U H4 H6).
-apply eventually_impl_base with (fun i:DS_set I => In U (x i));
+apply eventually_impl_base with (fun i:I => In U (x i));
   trivial.
 intros.
 assert (In (inverse_image f V) (x i)) by auto with sets.
@@ -249,7 +293,7 @@ Qed.
 Lemma func_preserving_net_limits_is_continuous:
   forall x0:X,
   (forall (I:DirectedSet) (x:Net I X),
-    net_limit x x0 -> net_limit (fun i:DS_set I => f (x i)) (f x0))
+    net_limit x x0 -> net_limit (fun i:I => f (x i)) (f x0))
   -> continuous_at f x0.
 Proof.
 intros.
@@ -279,48 +323,42 @@ Lemma subnet_limit: forall (x0:X) {J:DirectedSet}
   net_limit y x0.
 Proof.
 intros.
-destruct H0.
-red. intros.
-destruct (H U H2 H3).
-destruct (H1 x1).
-destruct H5, H6.
-exists x3.
-intros.
-apply H4.
-apply preord_trans with x2; trivial.
-- apply DS_ord_cond.
-- rewrite <- H6.
-  now apply H0.
+destruct H0 as [h [Hh0 [Hh1 Hxy]]].
+red. intros U HU HUx0.
+destruct (H U HU HUx0) as [i Hi].
+destruct (Hh1 i) as [i0 [Hii [j0 Hij0]]].
+subst i0. exists j0.
+intros j1 Hj1.
+rewrite Hxy. apply Hi.
+apply preord_trans with (h j0); auto.
+apply DS_ord_cond.
 Qed.
 
 Lemma subnet_cluster_point: forall (x0:X) {J:DirectedSet}
   (y:Net J X), net_cluster_point y x0 ->
   Subnet x y -> net_cluster_point x x0.
 Proof.
 intros.
-destruct H0 as [h h_increasing h_dominant].
-red. intros.
-red. intros.
-destruct (h_dominant i).
-destruct H2, H3.
-destruct (H U H0 H1 x2).
-destruct H4.
-exists (h x3).
-split; trivial.
-apply preord_trans with x1; trivial.
-- apply DS_ord_cond.
-- rewrite <- H3.
-  now apply h_increasing.
+destruct H0 as [h [h_increasing [h_dominant Hxy]]].
+intros U HU HUx0 i.
+destruct (h_dominant i) as [i0 [Hii [j Hj]]].
+subst i0.
+destruct (H U HU HUx0 j) as [j0 [Hj0 Hj1]].
+exists (h j0).
+split.
+- apply preord_trans with (h j); auto.
+  apply DS_ord_cond.
+- rewrite <- Hxy. assumption.
 Qed.
 
 Section cluster_point_subnet.
 
 Variable x0:X.
 Hypothesis x0_cluster_point: net_cluster_point x x0.
-Hypothesis I_nonempty: inhabited (DS_set I).
+Hypothesis I_nonempty: inhabited I.
 
 Record cluster_point_subnet_DS_set : Type := {
-  cps_i:DS_set I;
+  cps_i:I;
   cps_U:Ensemble X;
   cps_U_open_neigh: open_neighborhood cps_U x0;
   cps_xi_in_U: In cps_U (x cps_i)
@@ -389,27 +427,29 @@ Defined.
 
 Definition cluster_point_subnet : Net
   cluster_point_subnet_DS X :=
-  fun (iU:DS_set cluster_point_subnet_DS) =>
+  fun (iU : cluster_point_subnet_DS) =>
   x (cps_i iU).
 
 Lemma cluster_point_subnet_is_subnet:
   Subnet x cluster_point_subnet.
 Proof.
-constructor.
-- intros.
+exists cps_i. split; [|split].
+- intros j1 j2.
   destruct j1, j2.
-  simpl in H. simpl.
-  red in H. tauto.
-- red. intros.
-  exists i. split.
+  simpl. intros Hjj.
+  unfold cluster_point_subnet_DS_ord in Hjj at 1.
+  cbn in Hjj. tauto.
+- intros i. exists i. split.
   + apply preord_refl, DS_ord_cond.
   + assert (open_neighborhood Full_set x0).
     { repeat constructor.
-      apply open_full. }
+      apply open_full.
+    }
     assert (In Full_set (x i)) by
       constructor.
     now exists (Build_cluster_point_subnet_DS_set
       i Full_set H H0).
+- intros j. reflexivity.
 Qed.
 
 Lemma cluster_point_subnet_converges:

theories/Topology/ProductTopology.v

@@ -24,8 +24,8 @@ Qed.
 
 Lemma product_net_limit: forall (I:DirectedSet)
   (x:Net I ProductTopology) (x0:ProductTopology),
-  inhabited (DS_set I) ->
-  (forall a:A, net_limit (fun i:DS_set I => x i a) (x0 a)) ->
+  inhabited I ->
+  (forall a:A, net_limit (fun i:I => x i a) (x0 a)) ->
   net_limit x x0.
 Proof.
 intros.
@@ -215,8 +215,8 @@ apply net_limit_in_projections_impl_net_limit_in_weak_topology.
       now destruct (x0 i).
   + unfold product_space_proj.
     simpl.
-    replace (fun i:DS_set I => prod2_conv2 (x0 i) twoT_2) with
-      (fun i:DS_set I => snd (x0 i)).
+    replace (fun i:I => prod2_conv2 (x0 i) twoT_2) with
+      (fun i:I => snd (x0 i)).
     * now apply net_limit_in_weak_topology_impl_net_limit_in_projections
         with (a:=twoT_2) in H.
     * extensionality i.