X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fdama%2Fdama_didactic%2Fsequences.ma;fp=matita%2Fcontribs%2Fdama%2Fdama_didactic%2Fsequences.ma;h=7e558030caee8edfa366577fcb70ec577fdaac1d;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/dama/dama_didactic/sequences.ma b/matita/contribs/dama/dama_didactic/sequences.ma
new file mode 100644
index 000000000..7e558030c
--- /dev/null
+++ b/matita/contribs/dama/dama_didactic/sequences.ma
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+
+include "reals.ma".
+
+axiom continuo: (R → R) → Prop.
+axiom tends_to: (nat → R) → R → Prop.
+axiom tends_to_inf: (nat → R) → Prop.
+
+definition monotone_not_increasing ≝
+ λ alpha:nat→R.
+ ∀n:nat.alpha (S n) ≤ alpha n.
+
+definition inf_bounded ≝
+ λ alpha:nat → R.
+ ∃ m. ∀ n:nat. m ≤ alpha n.
+
+axiom converge: ∀ alpha.
+ monotone_not_increasing alpha →
+ inf_bounded alpha →
+ ∃ l. tends_to alpha l.
+
+definition punto_fisso :=
+ λ F:R→R. λ x. x = F x.
+
+let rec successione F x (n:nat) on n : R ≝
+ match n with
+  [ O ⇒ x
+  | S n ⇒ F (successione F x n)
+  ].
+
+axiom lim_punto_fisso:
+∀ F: R → R. ∀b:R. continuo F →
+ let alpha := successione F b in
+  ∀ l. tends_to alpha l →
+    punto_fisso F l.
+
+definition monotone_not_decreasing ≝
+ λ alpha:nat→R.
+ ∀n:nat.alpha n ≤ alpha (S n).
+ 
+definition sup_bounded ≝
+ λ alpha:nat → R.
+ ∃ m. ∀ n:nat. alpha n ≤ m.