1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/ordered_sets2".
17 include "ordered_sets.ma".
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'.
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;
32 apply (inf_greatest_lower_bound ? ? ? ? (inf_is_inf ? ? ?));
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);
42 [ apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? ?));
43 | apply (or_reflexive ? O' (dscos_ordered_set ? O'))
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.
53 apply (sup_least_upper_bound ? ? ? ? (sup_is_sup ? ? a));
56 apply (or_transitive ? ? O');
59 | apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? b))
63 interpretation "mk_bounded_sequence" 'hide_everything_but a
64 = (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
67 ∀C.∀O':dedekind_sigma_complete_ordered_set C.
68 ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
69 ∀a:bounded_sequence ? O'.
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)
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)
84 rewrite > eq_f_liminf_sup_f_inf;
86 apply le_to_le_sup_sup;
87 elim daemon (*(* f inf < inf f *)
88 apply le_f_inf_inf_f*)