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=ca5c21576ebd9a7bc9569cb8d713a9220392f2cf;hp=4b53407d1f11e95c6b0deb713a597bef3ee653c9;hpb=2857d1c432f073379552e1572235a86509b665a4;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 4b53407d1..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,11 +24,6 @@ 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);
@@ -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).