]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/dama_didactic/sequences.ma
Axiom moved from ex_deriv to deriv where it belongs to.
[helm.git] / helm / software / matita / dama_didactic / sequences.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/didactic/sequences".
16
17 include "reals.ma".
18
19 axiom continuo: (R → R) → Prop.
20 axiom tends_to: (nat → R) → R → Prop.
21 axiom tends_to_inf: (nat → R) → Prop.
22
23 definition monotone_not_increasing ≝
24  λ alpha:nat→R.
25  ∀n:nat.alpha (S n) ≤ alpha n.
26
27 definition inf_bounded ≝
28  λ alpha:nat → R.
29  ∃ m. ∀ n:nat. m ≤ alpha n.
30
31 axiom converge: ∀ alpha.
32  monotone_not_increasing alpha →
33  inf_bounded alpha →
34  ∃ l. tends_to alpha l.
35
36 definition punto_fisso :=
37  λ F:R→R. λ x. x = F x.
38
39 let rec successione F x (n:nat) on n : R ≝
40  match n with
41   [ O ⇒ x
42   | S n ⇒ F (successione F x n)
43   ].
44
45 axiom lim_punto_fisso:
46 ∀ F: R → R. ∀b:R. continuo F →
47  let alpha := successione F b in
48   ∀ l. tends_to alpha l →
49     punto_fisso F l.
50
51 definition monotone_not_decreasing ≝
52  λ alpha:nat→R.
53  ∀n:nat.alpha n ≤ alpha (S n).
54  
55 definition sup_bounded ≝
56  λ alpha:nat → R.
57  ∃ m. ∀ n:nat. alpha n ≤ m.