matita/dama/ordered_sets2.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 set "baseuri" "cic:/matita/ordered_sets2".
  16
  17 include "ordered_sets.ma".
  18
  19 theorem le_f_inf_inf_f:
  20  ∀C.∀O':dedekind_sigma_complete_ordered_set C.
  21   ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
  22    ∀a:bounded_below_sequence ? O'.
  23     let p := ? in
  24      f (inf ? ? a) ≤ inf ? ? (mk_bounded_below_sequence ? ? (λi. f (a i)) p).
  25  [ apply mk_is_bounded_below;
  26     [2: apply ioc_is_lower_bound_f_inf;
  27         assumption
  28     | skip
  29     ]
  30  | intros;
  31    clearbody p;
  32    apply (inf_greatest_lower_bound ? ? ? ? (inf_is_inf ? ? ?));
  33    simplify;
  34    intro;
  35    letin b := (λi.match i with [ O ⇒ inf ? ? a | S _ ⇒ a n]);
  36    change with (f (b O) ≤ f (b (S O)));
  37    apply (ioc_is_sequentially_monotone ? ? ? H);
  38    simplify;
  39    clear b;
  40    intro;
  41    elim n1; simplify;
  42     [ apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? ?));
  43     | apply (or_reflexive ? O' (dscos_ordered_set ? O'))
  44     ]
  45  ].
  46 qed.
  47
  48 theorem le_to_le_sup_sup:
  49  ∀C.∀O':dedekind_sigma_complete_ordered_set C.
  50   ∀a,b:bounded_above_sequence ? O'.
  51    (∀i.a i ≤ b i) → sup ? ? a ≤ sup ? ? b.
  52  intros;
  53  apply (sup_least_upper_bound ? ? ? ? (sup_is_sup ? ? a));
  54  unfold;
  55  intro;
  56  apply (or_transitive ? ? O');
  57   [2: apply H
  58   | skip
  59   | apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? b))
  60   ].
  61 qed.
  62
  63 interpretation "mk_bounded_sequence" 'hide_everything_but a
  64 = (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
  65
  66 theorem fatou:
  67  ∀C.∀O':dedekind_sigma_complete_ordered_set C.
  68   ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
  69    ∀a:bounded_sequence ? O'.
  70     let pb := ? in
  71     let pa := ? in
  72      f (liminf ? ? a) ≤ liminf ? ? (mk_bounded_sequence ? ? (λi. f (a i)) pb pa).
  73  [ letin bas ≝ (bounded_above_sequence_of_bounded_sequence ? ? a);
  74    apply mk_is_bounded_above;
  75     [2: apply (ioc_is_upper_bound_f_sup ? ? ? H bas)
  76     | skip
  77     ]
  78  | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? ? a);
  79    apply mk_is_bounded_below;
  80     [2: apply (ioc_is_lower_bound_f_inf ? ? ? H bbs)
  81     | skip
  82     ]
  83  | intros;
  84    rewrite > eq_f_liminf_sup_f_inf;
  85     [ unfold liminf;
  86       apply le_to_le_sup_sup;
  87       elim daemon (*(* f inf < inf f *)
  88       apply le_f_inf_inf_f*)
  89     | assumption
  90     ]
  91  ].
  92 qed.