Add EuclideanSpaces.v to _CoqProject & fix error

coq-community · Feb 7, 2021 · 6b24418 · 6b24418
1 parent 091e254
commit 6b24418
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/_CoqProject b/_CoqProject
@@ -8,6 +8,7 @@ theories/Topology/Connectedness.v
 theories/Topology/Continuity.v
 theories/Topology/ContinuousFactorization.v
 theories/Topology/CountabilityAxioms.v
+theories/Topology/EuclideanSpaces.v
 theories/Topology/FilterLimits.v
 theories/Topology/FiltersAndNets.v
 theories/Topology/Homeomorphisms.v

diff --git a/theories/Topology/EuclideanSpaces.v b/theories/Topology/EuclideanSpaces.v
@@ -303,7 +303,7 @@ Lemma compact_Subspace (X : TopologicalSpace) (S : Ensemble (point_set X)) :
     (forall U, In C U -> open U) ->
     FamilyUnion C = Full_set ->
     exists C',
-      Finite _ C' /\ Included C' C /\ Included S (FamilyUnion C').
+      Finite C' /\ Included C' C /\ Included S (FamilyUnion C').
 Proof.
   intros.
   unshelve edestruct H as [C'].