Declare DirectedSets.DS_set as coercion

The coercion from `DirectedSets` to `Sortclass` makes some code easier
to write.

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.
@@ -380,14 +380,14 @@ apply net_cluster_point_impl_subnet_converges in H6.
 }
 destruct H6 as [J [y' [HySy' Hy']]].
 destruct HySy' as [h [Hh0 [Hh1 Hhy']]].
-assert (net_limit (fun j:DS_set J => y (h j)) x0).
+assert (net_limit (fun j:J => y (h j)) x0).
 { apply continuous_func_preserves_net_limits with
   (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.
   exists h. now constructor. }
 assert (x = x0).
@@ -443,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 cauchy (x:nat->X) : Prop :=
 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) :

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 @@ Qed.
 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 @@ Lemma metric_space_net_limit_converse: forall (X:TopologicalSpace)
   (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 @@ Lemma metric_space_net_cluster_point: forall (X:TopologicalSpace)
   (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 @@ Lemma metric_space_net_cluster_point_converse: forall (X:TopologicalSpace)
   (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).

theories/Topology/Nets.v

@@ -4,18 +4,18 @@ 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 : DS_set J -> DS_set I),
+  exists (h : J -> I),
     (* [h] is monotonous *)
-    (forall j1 j2 : DS_set J,
+    (forall j1 j2 : 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) /\
+    (exists arbitrarily large i : I,
+      exists j : J, h j = i) /\
     (* [y] is [x ∘ h] *)
-    (forall j : DS_set J,
+    (forall j : J,
         y j = x (h j)).
 
 Lemma Subnet_refl {I : DirectedSet} {X : Type} (x : Net I X) :
@@ -54,14 +54,14 @@ 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 : DS_set I, x1 i = x2 i) ->
+  (forall i : I, x1 i = x2 i) ->
   net_limit x1 x -> net_limit x2 x.
 Proof.
   intros Hxx Hx1.
@@ -87,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.
@@ -105,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.
@@ -192,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 ->
@@ -273,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 ? ?.
@@ -283,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.
@@ -293,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.
@@ -355,10 +355,10 @@ 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)
@@ -427,7 +427,7 @@ 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:

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.

theories/Topology/RTopology.v

@@ -173,21 +173,21 @@ exists R_metric.
 Qed.
 
 Lemma bounded_real_net_has_cluster_point: forall (I:DirectedSet)
-  (x:Net I RTop) (a b:R), (forall i:DS_set I, a <= x i <= b) ->
+  (x:Net I RTop) (a b:R), (forall i:I, a <= x i <= b) ->
   exists x0:RTop, net_cluster_point x x0.
 Proof.
 (* idea: the liminf is a cluster point *)
 intros.
-destruct (classic (inhabited (DS_set I))) as [Hinh|Hempty].
+destruct (classic (inhabited I)) as [Hinh|Hempty].
 2: {
   exists a.
   red. intros.
   red. intros.
   contradiction Hempty.
   now exists.
 }
-assert (forall i:DS_set I, { y:R | is_glb
-                           (Im [ j:DS_set I | DS_ord i j ] x) y }).
+assert (forall i:I, { y:R | is_glb
+                         (Im [ j:I | DS_ord i j ] x) y }).
 { intro.
   apply inf.
   - exists a.
@@ -221,7 +221,7 @@ assert ({ x0:R | is_lub (Im Full_set (fun i => proj1_sig (X i))) x0 }).
 }
 destruct H0 as [x0].
 exists x0.
-assert (forall i j:DS_set I,
+assert (forall i j:I,
            DS_ord i j -> proj1_sig (X i) <= proj1_sig (X j)).
 { intros.
   destruct (X i0), (X j).
@@ -283,7 +283,7 @@ Proof.
 intros a b Hbound.
 apply net_cluster_point_impl_compact.
 intros.
-pose (y := fun i:DS_set I => proj1_sig (x i)).
+pose (y := fun i:I => proj1_sig (x i)).
 destruct (bounded_real_net_has_cluster_point _ y a b).
 { intros.
   unfold y.

theories/Topology/WeakTopology.v

@@ -71,13 +71,13 @@ Qed.
 Section WeakTopology_and_Nets.
 
 Variable I:DirectedSet.
-Hypothesis I_nonempty: inhabited (DS_set I).
+Hypothesis I_nonempty: inhabited I.
 Variable x:Net I WeakTopology.
 Variable x0:X.
 
 Lemma net_limit_in_weak_topology_impl_net_limit_in_projections :
   net_limit x x0 ->
-  forall a:A, net_limit (fun i:DS_set I => (f a) (x i)) ((f a) x0).
+  forall a:A, net_limit (fun i:I => (f a) (x i)) ((f a) x0).
 Proof.
 intros.
 apply continuous_func_preserves_net_limits; trivial.
@@ -86,7 +86,7 @@ apply weak_topology_makes_continuous_funcs.
 Qed.
 
 Lemma net_limit_in_projections_impl_net_limit_in_weak_topology :
-  (forall a:A, net_limit (fun i:DS_set I => (f a) (x i))
+  (forall a:A, net_limit (fun i:I => (f a) (x i))
                          ((f a) x0)) ->
   net_limit x x0.
 Proof.
@@ -96,19 +96,19 @@ assert (@open_basis WeakTopology
         (finite_intersections weak_topology_subbasis)).
 { apply Build_TopologicalSpace_from_open_basis_basis. }
 destruct (open_basis_cover _ H2 x0 U) as [V [? [? ?]]]; trivial.
-assert (for large i:DS_set I, In V (x i)).
+assert (for large i:I, In V (x i)).
 { clear H4.
   induction H3.
   - destruct I_nonempty.
     exists X0; constructor.
   - destruct H3.
     destruct H5.
-    apply eventually_impl_base with (fun i:DS_set I => In V (f a (x i))).
+    apply eventually_impl_base with (fun i:I => In V (f a (x i))).
     + intros.
       constructor; trivial.
     + apply H; trivial.
   - apply eventually_impl_base with
-        (fun i:DS_set I => In U0 (x i) /\ In V (x i)).
+        (fun i:I => In U0 (x i) /\ In V (x i)).
     + intros.
       destruct H6.
       constructor; trivial.