notation made half decent

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / saturations_to_o-saturations.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
index 88a18fda7a38ecd5f8750f8b7d6e3bb1fe0a42b7..0a67005681662c1e7b74fb98eb39af7aa13c5302 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
@@ -18,19 +18,16 @@ include "relations_to_o-algebra.ma".
 
 (* These are only conversions :-) *)
 
-definition o_operator_of_operator:
- ∀C:REL. (Ω \sup C => Ω \sup C) → (POW C ⇒ POW C).
+definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)).
  intros (C t);apply t;
 qed.
 
-definition is_o_saturation_of_is_saturation:
- ∀C:REL.∀R: unary_morphism1 (Ω \sup C) (Ω \sup C).
+definition is_o_saturation_of_is_saturation: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
   is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
  intros; apply i;
 qed.
 
-definition is_o_reduction_of_is_reduction:
- ∀C:REL.∀R: unary_morphism1 (Ω \sup C) (Ω \sup C).
+definition is_o_reduction_of_is_reduction: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
   is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
  intros; apply i;
 qed.
\ No newline at end of file