[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification real-limit
enrich
   real-supinf, 
   real-multdiv, 
   nat
with
   predicates 
       converges : (Nat → Real);
       converges : (Nat → Real) × Real;
       mon≤ : (Nat → Real);
       mon≥ : (Nat → Real);
       bounded≤ : (Nat → Real) × Real;
       bounded≥ : (Nat → Real) × Real;
   
   variables 
       f : Nat → Real;
       r : Real;
       ε : Real;
       n : Nat;
       i : Int;
       j : Int;
   
   partial functions 
       limit : (Nat → Real) → Real with λ f. converges(f);
   
   
   axioms 
      monle-def: mon≤(f) ↔ (∀ n, n0. n ≤ n0 → f(n) ≤ f(n0));
      
      monge-def: mon≥(f) ↔ (∀ n, n0. n ≤ n0 → f(n) ≥ f(n0));
      
      boundedle-def: bounded≤(f, r) ↔ (∀ n. f(n) ≤ r);
      
      boundedge-def: bounded≥(f, r) ↔ (∀ n. f(n) ≥ r);
      
      convergesto-def: converges(f, r) ↔ (∀ ε. ε > 0.r → (∃ n. ∀ n0. n0 ≥ n → abs(f(n0) - r) < ε));
      
      converges-def: converges(f) ↔ (∃ r. converges(f, r));
      
      limit-def: converges(f) ⊦ converges(f, limit(f));
   
   theorems 
      limit-unique: converges(f, r0) → (converges(f, r1) ↔ r0 = r1);
      comment: justifies definition of limit;
   
   
end enrich