]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/dama/sandwich.ma
more ex and more notation
[helm.git] / helm / software / matita / library / dama / sandwich.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "dama/ordered_uniform.ma".
16
17 lemma le_w_plus: ∀n,m,o.n+m≤o → m ≤ o.
18 intro; elim n; simplify; [assumption]
19 lapply (le_S ?? H1); apply H; apply le_S_S_to_le; assumption;
20 qed.
21
22 alias symbol "leq" = "Ordered set less or equal than".
23 alias symbol "and" = "logical and".
24 theorem sandwich: 
25   ∀O:ordered_uniform_space.∀l:O.∀a,b,x:sequence O.
26    (∀i:nat.a i ≤ x i ∧ x i ≤ b i) →
27     a uniform_converges l → 
28      b uniform_converges l → 
29       x uniform_converges l.
30 intros 10; 
31 cases (us_phi3 ? ? H3) (V GV); cases GV (Gv HV); clear GV;
32 cases (us_phi3 ? ? Gv) (W GW); cases GW (Gw HW); clear GW;
33 cases (H1 ? Gw) (ma Hma); cases (H2 ? Gw) (mb Hmb); clear H1 H2;
34 exists [apply (ma + mb)] intros; apply (HV 〈l,(x i)〉); 
35 unfold; simplify; exists [apply (a i)] split;
36 [2: apply (ous_convex_l ?? Gv 〈a i,b i〉); cases (H i) (Lax Lxb); clear H;
37     [1: apply HW; exists [apply l]simplify; split; 
38         [1: cases (us_phi4 ?? Gw 〈(a i),l〉); apply H2; clear H2 H;
39             apply (Hma i); rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;
40         |2: apply Hmb; apply (le_w_plus ma); assumption] 
41     |2,3: simplify; apply (le_transitive (a i) ?? Lax Lxb);
42     |4: apply (le_reflexive);
43     |5,6: assumption;]
44 |1: apply HW; exists[apply l] simplify; split;
45     [1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive;
46     |2: apply Hma;  rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;]]
47 qed. 
48