...

[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 4c725920bf6346820039542707a98260e25a29dd..2fb7a6b1d6c3bd297c774f85130546b3d45d5621 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
@@ -15,20 +15,17 @@
 include "o-algebra.ma".
 include "o-saturations.ma".
 
-record Obasic_topology: Type2 ≝
- { Ocarrbt:> OA;
-   oA: Ocarrbt ⇒_2 Ocarrbt;
-   oJ: Ocarrbt ⇒_2 Ocarrbt;
-   oA_is_saturation: is_o_saturation ? oA;
-   oJ_is_reduction: is_o_reduction ? oJ;
+record Obasic_topology: Type2 ≝ { 
+   Ocarrbt:> OA;
+   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) =_1 (U >< oJ V)
  }.
 
-record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝
- { Ocont_rel:> arrows2 OA S T;
-   (* reduces uses eq1, saturated uses eq!!! *)
-   Oreduced: ∀U. U = oJ ? U → Ocont_rel U = oJ ? (Ocont_rel U);
-   Osaturated: ∀U. U = oA ? U → Ocont_rel⎻* U = oA ? (Ocont_rel⎻* U)
+record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝ { 
+   Ocont_rel:> arrows2 OA S T;
+   Oreduced: ∀U:S. U = oJ ? U → Ocont_rel U =_1 oJ ? (Ocont_rel U);
+   Osaturated: ∀U:S. U = oA ? U → Ocont_rel⎻* U =_1 oA ? (Ocont_rel⎻* U)
  }. 
 
 definition Ocontinuous_relation_setoid: Obasic_topology → Obasic_topology → setoid2.