- new notation.ma file with local and common notation

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
index 8555cf00acc5ef5feccafb32c68e827f076866b0..b78e7b037046bededec4973267647e8e115270bc 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
@@ -18,10 +18,10 @@ include "o-basic_topologies.ma".
 alias symbol "eq" = "setoid1 eq".
 
 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
-definition o_basic_topology_of_o_basic_pair: BP → BTop.
+definition o_basic_topology_of_o_basic_pair: OBP → BTop.
  intro t;
  constructor 1;
-  [ apply (form t);
+  [ apply (Oform t);
   | apply (□_t ∘ Ext⎽t);
   | apply (◊_t ∘ Rest⎽t);
   | intros 2; split; intro;
@@ -58,7 +58,7 @@ definition o_basic_topology_of_o_basic_pair: BP → BTop.
 qed.
 
 definition o_continuous_relation_of_o_relation_pair:
- ∀BP1,BP2.arrows2 BP BP1 BP2 →
+ ∀BP1,BP2.arrows2 OBP BP1 BP2 →
   arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
  intros (BP1 BP2 t);
  constructor 1;
@@ -68,7 +68,7 @@ definition o_continuous_relation_of_o_relation_pair:
     apply (.= †(†e));
     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
     cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
-      cases (commute ?? t); apply (e3 ^ -1 ((⊩)* U));]
+      cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩)* U));]
     apply (.= †COM);
     change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
     apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
@@ -81,7 +81,7 @@ definition o_continuous_relation_of_o_relation_pair:
     apply (.= †(†e));
     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
     cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
-      cases (commute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
+      cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
     apply (.= †COM);
     change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
     apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));