more notation

[helm.git] / helm / software / matita / library / formal_topology / relations_to_o-algebra.ma

diff --git a/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma b/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma
index 3a908657bb05f7d7fec3bd6c05572f5773eaaf16..93bf2c609694693c0bb14b99fb3627cc6b47d0bd 100644 (file)
--- a/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma
+++ b/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma
@@ -170,10 +170,8 @@ definition POW: carr3 (arrows3 CAT2 (category2_of_category1 REL) OA).
   | apply orelation_of_relation_preserves_composition; ]
 qed.
 
-theorem POW_faithful:
- ∀S,T.∀f,g:arrows2 (category2_of_category1 REL) S T.
-   POW⎽⇒ f =_2 POW⎽⇒ g → f =_2 g.
- intros; unfold POW in e; simplify in e; cases e;
+theorem POW_faithful: faithful2 ?? POW.
+ intros 5; unfold POW in e; simplify in e; cases e;
  unfold orelation_of_relation in e3; simplify in e3; clear e e1 e2 e4;
  intros 2; cases (e3 {(x)}); 
  split; intro; [ lapply (s y); | lapply (s1 y); ]
@@ -181,13 +179,14 @@ theorem POW_faithful:
   |*: cases Hletin; cases x1; change in f3 with (x =_1 w); apply (. f3‡#); assumption;]
 qed.
 
-
+(*
 lemma currify: ∀A,B,C. (A × B ⇒_1 C) → A → (B ⇒_1 C).
 intros; constructor 1; [ apply (b c); | intros; apply (#‡e);]
 qed.
+*)
 
-theorem POW_full: ∀S,T.∀f: (POW S) ⇒_\o2 (POW T) . exT22 ? (λg. POW⎽⇒ g = f).
- intros; exists;
+theorem POW_full: full2 ?? POW. 
+ intros 3 (S T); exists;
   [ constructor 1; constructor 1;
      [ apply (λx:carr S.λy:carr T. y ∈ f {(x)});
      | intros; unfold FunClass_1_OF_carr2; lapply (.= e1‡#);