notation made half decent

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-basic_topologies.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
index 245fc4fdbf866ee9c9a28d521bb790c5f5cf4489..4c725920bf6346820039542707a98260e25a29dd 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -17,11 +17,11 @@ include "o-saturations.ma".
 
 record Obasic_topology: Type2 ≝
  { Ocarrbt:> OA;
-   oA: Ocarrbt ⇒ Ocarrbt;
-   oJ: Ocarrbt ⇒ Ocarrbt;
+   oA: Ocarrbt ⇒_2 Ocarrbt;
+   oJ: Ocarrbt ⇒_2 Ocarrbt;
    oA_is_saturation: is_o_saturation ? oA;
    oJ_is_reduction: is_o_reduction ? oJ;
-   Ocompatibility: ∀U,V. (oA U >< oJ V) = (U >< oJ V)
+   Ocompatibility: ∀U,V. (oA U >< oJ V) =_1 (U >< oJ V)
  }.
 
 record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝
@@ -134,11 +134,11 @@ definition OBTop: category2.
        change in e1 with (b⎻* ∘ oA o2 = b'⎻* ∘ oA o2);
        apply (.= e‡#);
        intro x;          
-       change with (eq1 ? (b⎻* (a'⎻* (oA o1 x))) (b'⎻*(a'⎻* (oA o1 x)))); 
+       change with (b⎻* (a'⎻* (oA o1 x)) =_1 b'⎻*(a'⎻* (oA o1 x))); 
        apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [
          apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
        apply (.= (e1 (a'⎻* (oA o1 x))));
-       change with (eq1 ? (b'⎻* (oA o2 (a'⎻* (oA o1 x)))) (b'⎻*(a'⎻* (oA o1 x))));   
+       change with (b'⎻* (oA o2 (a'⎻* (oA o1 x))) =_1 b'⎻*(a'⎻* (oA o1 x)));   
        apply (.= †(Osaturated o1 o2 a' (oA o1 x):?)^-1); [
          apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
        apply rule #;]