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 lemma reduce_bas_seq:
  67  ∀C.∀O:ordered_set C.∀a:nat→O.∀p.∀i.
  68   bas_seq ? ? (mk_bounded_above_sequence ? ? a p) i = a i.
  69  intros;
  70  reflexivity.
  71 qed.
  72
  73 (*lemma reduce_bbs_seq:
  74  ∀C.∀O:ordered_set C.∀a:nat→O.∀p.∀i.
  75   bbs_seq ? ? (mk_bounded_below_sequence ? ? a p) i = a i.
  76  intros;
  77  reflexivity.
  78 qed.*)
  79
  80 axiom inf_extensional:
  81  ∀C.∀O:dedekind_sigma_complete_ordered_set C.
  82   ∀a,b:bounded_below_sequence ? O.
  83    (∀i.a i = b i) → inf ? ? a = inf ? O b.
  84
  85 lemma eq_to_le: ∀C.∀O:ordered_set C.∀x,y:O.x=y → x ≤ y.
  86  intros;
  87  rewrite > H;
  88  apply (or_reflexive ? ? O).
  89 qed.
  90
  91 theorem fatou:
  92  ∀C.∀O':dedekind_sigma_complete_ordered_set C.
  93   ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
  94    ∀a:bounded_sequence ? O'.
  95     let pb := ? in
  96     let pa := ? in
  97      f (liminf ? ? a) ≤ liminf ? ? (mk_bounded_sequence ? ? (λi. f (a i)) pb pa).
  98  [ letin bas ≝ (bounded_above_sequence_of_bounded_sequence ? ? a);
  99    apply mk_is_bounded_above;
 100     [2: apply (ioc_is_upper_bound_f_sup ? ? ? H bas)
 101     | skip
 102     ]
 103  | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? ? a);
 104    apply mk_is_bounded_below;
 105     [2: apply (ioc_is_lower_bound_f_inf ? ? ? H bbs)
 106     | skip
 107     ]
 108  | intros;
 109    rewrite > eq_f_liminf_sup_f_inf in ⊢ (? ? ? % ?);
 110     [ unfold liminf;
 111       apply le_to_le_sup_sup;
 112       intro;
 113       rewrite > reduce_bas_seq;
 114       rewrite > reduce_bas_seq;
 115       apply (or_transitive ? O' O');
 116        [2: apply le_f_inf_inf_f;
 117            assumption
 118        | skip
 119        | apply eq_to_le;
 120          apply inf_extensional;
 121          intro;
 122          reflexivity
 123        ]
 124     | assumption
 125     ]
 126  ].
 127 qed.