X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_topologies.ma;h=013ddb94d5a15db81551249caca71610974733a2;hb=a484c51de8ba6c56f02f9c0758688d3c9186b63d;hp=26562cbb41805565c6eec931d6c7ad488ba3c325;hpb=5be81fce195f2b45ec57c5422d35e4c03827891d;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
index 26562cbb4..013ddb94d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
@@ -24,17 +24,12 @@ record basic_topology: Type1 ≝
    compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V)
  }.
 
-lemma hint: basic_topology → objs1 REL.
- intro; apply (carrbt b);
-qed.
-coercion hint.
-
 record continuous_relation (S,T: basic_topology) : Type1 ≝
  { cont_rel:> arrows1 ? S T;
    reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
    saturated: ∀U. U = A ? U → minus_star_image ?? cont_rel U = A ? (minus_star_image ?? cont_rel U)
  }. 
-
+(*
 definition continuous_relation_setoid: basic_topology → basic_topology → setoid1.
  intros (S T); constructor 1;
   [ apply (continuous_relation S T)
@@ -45,14 +40,6 @@ definition continuous_relation_setoid: basic_topology → basic_topology → set
      | simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]]
 qed.
 
-definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel.
-
-coercion cont_rel'.
-
-definition cont_rel'': ∀S,T: basic_topology. continuous_relation_setoid S T → binary_relation S T ≝ cont_rel.
-
-coercion cont_rel''.
-
 theorem continuous_relation_eq':
  ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
   a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X).
@@ -202,4 +189,5 @@ theorem continuous_relation_eqS:
   [2,4: intros; apply saturation_monotone; try (apply A_is_saturation); apply Hcut;]
  apply Hcut2; assumption.
 qed.
+*)
 *)
\ No newline at end of file