]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/dama/dama/ordered_uniform.ma
Another bug.
[helm.git] / helm / software / matita / contribs / dama / dama / ordered_uniform.ma
index 1dba15a7c00242c47bccee31ea638411660af3bf..5d6559d1f301a5ad0c51de2a32a920b18a592cf3 100644 (file)
@@ -78,20 +78,17 @@ lemma restriction_agreement :
   ∀O:ordered_uniform_space.∀s:‡O.∀P:{[s]} squareO → Prop.∀OP:O squareO → Prop.Prop.
 apply(λO:ordered_uniform_space.λs:‡O.
        λP:{[s]} squareO → Prop. λOP:O squareO → Prop.
-          ∀b:O squareO.∀H1,H2.(P b → OP b) ∧ (OP b → P b));
-[5,7: apply H1|6,8:apply H2]skip;
+          ∀b:{[s]} squareO.(P b → OP b) ∧ (OP b → P b));
 qed.
 
 lemma unrestrict: ∀O:ordered_uniform_space.∀s:‡O.∀U,u.∀x:{[s]} squareO.
   restriction_agreement ? s U u → U x → u x.
-intros 6; cases x (b b1); cases b (w1 H1); cases b1 (w2 H2); clear b b1 x; 
-cases (H 〈w1,w2〉 H1 H2) (L _); intro Uw; apply L; apply Uw;
+intros 6; cases (H x); assumption;
 qed.
 
 lemma restrict: ∀O:ordered_uniform_space.∀s:‡O.∀U,u.∀x:{[s]} squareO.
   restriction_agreement ? s U u → u x → U x.
-intros 5; cases x (b b1); cases b (w1 H1); cases b1 (w2 H2); clear b1 b x;
-intros (Ra uw); cases (Ra 〈w1,w2〉 H1 H2) (_ R); apply R; apply uw;
+intros 6; cases (H x); assumption;
 qed.
 
 lemma invert_restriction_agreement: 
@@ -99,9 +96,9 @@ lemma invert_restriction_agreement:
    ∀U:{[s]} squareO → Prop.∀u:O squareO → Prop.
     restriction_agreement ? s U u →
     restriction_agreement ? s (\inv U) (\inv u).
-intros 8; split; intro;
-[1: apply (unrestrict ???? (segment_square_of_ordered_set_square ?? 〈\snd b,\fst b〉 H2 H1) H H3);
-|2: apply (restrict ???? (segment_square_of_ordered_set_square ?? 〈\snd b,\fst b〉 H2 H1) H H3);]
+intros 6; cases b;
+generalize in match (H 〈h1,h〉); cases h; cases h1; simplify; 
+intro X; cases X; split; assumption; 
 qed. 
 
 lemma bs2_of_bss2: 
@@ -202,7 +199,7 @@ intros (O s); apply mk_ordered_uniform_space;
 ]  
 qed.
 
-interpretation "Ordered uniform space segment" 'segment_set a = 
+interpretation "Ordered uniform space segment" 'segset a = 
  (segment_ordered_uniform_space _ a).
 
 (* Lemma 3.2 *)
@@ -210,7 +207,7 @@ alias symbol "pi1" = "exT \fst".
 lemma restric_uniform_convergence:
  ∀O:ordered_uniform_space.∀s:‡O.
   ∀x:{[s]}.
-   ∀a:sequence (segment_ordered_uniform_space O s).
+   ∀a:sequence {[s]}.
     (⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) → 
       a uniform_converges x.
 intros 7; cases H1; cases H2; clear H2 H1;