helm/software/matita/contribs/dama/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 "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 ?? 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: simplify; apply (le_transitive ???? Lax Lxb);
  42     |3: simplify; repeat split; try assumption;
  43         [1: apply (le_transitive ???? Lax Lxb);
  44         |2: intro X; cases (os_coreflexive ?? X)]]
  45 |1: apply HW; exists[apply l] simplify; split;
  46     [1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive;
  47     |2: apply Hma;  rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;]]
  48 qed.
  49