X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fsaturations_to_o-saturations.ma;h=4cbca05303ec7d6bd03389a94d4da28d182cd0d4;hb=05cfeb82d2624860e66941421a937f308d66cf33;hp=0a67005681662c1e7b74fb98eb39af7aa13c5302;hpb=7c4bb1d1baed259e4301d4cf0ecca7a0e3885d92;p=helm.git

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 0a6700568..4cbca0530 100644
--- 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,16 +18,12 @@ include "relations_to_o-algebra.ma".
 
 (* These are only conversions :-) *)
 
-definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)).
- intros (C t);apply t;
-qed.
+definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)) ≝ λC,t.t.
 
-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_saturation_of_is_saturation: 
+  ∀C:REL.∀R: Ω^C ⇒_1 Ω^C. is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
+intros (C R i); apply i; qed.
 
-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
+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 (C R i); apply i; qed.