big mess of notation

[helm.git] / helm / software / matita / library / formal_topology / basic_topologies_to_o-basic_topologies.ma

diff --git a/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma
index b1592f6eadf1e4d39ee775408ae75de1620a3509..0d997a5af617cf67b7947bc8fc5fe91cfb695ca8 100644 (file)
--- a/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma
+++ b/helm/software/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma
@@ -49,19 +49,43 @@ definition BTop_to_OBTop: carr3 ((category2_of_category1 BTop) ⇒_\c3 OBTop).
   | cases daemon (*apply o_relation_topology_of_relation_topology_morphism_respects_comp*);]
 qed.
 
-(*
+(* FIXME
 alias symbol "eq" (instance 2) = "setoid1 eq".
 alias symbol "eq" (instance 1) = "setoid2 eq".
-theorem BTop_to_OBTop_faithful:
- ∀S,T.∀f,g:arrows2 (category2_of_category1 BTop) S T.
-  map_arrows2 ?? BTop_to_OBTop ?? f = map_arrows2 ?? BTop_to_OBTop ?? g → f=g.
- intros; change with (∀b.A ? (ext ?? f b) = A ? (ext ?? g b));
- apply (POW_faithful);
- apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) f \sub \c (⊩ \sub T));
- apply sym2;
- apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) g \sub \c (⊩ \sub T));
- apply sym2;
- apply e;
+theorem BTop_to_OBTop_faithful: faithful2 ?? BTop_to_OBTop.
+ intros 5;
+ whd in e; unfold BTop_to_OBTop in e; simplify in e;
+ change in match (oA ?) in e with (A o1);
+ whd in f g;
+ alias symbol "OR_f_minus_star" (instance 1) = "relation f⎻*".
+ change in match ((o_continuous_relation_of_continuous_relation_morphism o1 o2 f)⎻* ) in e with ((foo ?? f)⎻* );
+ change in match ((o_continuous_relation_of_continuous_relation_morphism o1 o2 g)⎻* ) in e with ((foo ?? g)⎻* );
+ whd; whd in o1 o2;
+ intro b;
+ alias symbol "OR_f_minus" (instance 1) = "relation f⎻".
+ letin fb ≝ ((ext ?? f) b);
+ lapply (e fb);
+ whd in Hletin:(? ? ? % %);
+ cases (Hletin); simplify in s s1;
+ split;
+  [2: intro; simplify;
+    lapply depth=0 (s b); intro; apply (Hletin1 ? a ?)
+     [ 2: whd in f1;
+ change in Hletin with ((foo ?? f)⎻*
+ 
+ alias symbol "OR_f_minus_star" (instance 4) = "relation f⎻*".
+ alias symbol "OR_f_minus_star" (instance 4) = "relation f⎻*".
+change in e with
+ (comp2 SET1 (Ω^o1) (Ω^o1) (Ω^o2) (A o1) (foo o1 o2 f)⎻* =_1
+  comp2 SET1 (Ω^o1) (Ω^o1) (Ω^o2) (A o1) (foo o1 o2 g)⎻*
+ );
+ 
+ 
+ 
+ change in e with (comp1 SET (Ω^o1) ?? (A o1) (foo o1 o2 f)⎻*  = ((foo o1 o2 g)⎻* ∘ A o1));
+ unfold o_continuous_relation_of_continuous_relation_morphism in e;
+ unfold o_continuous_relation_of_continuous_relation in e;
+ simplify in e;
 qed.
 
 include "formal_topology/notation.ma".