[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-supinf
enrich
   real-abs
with
   predicates 
       bounded≤ : (Real → Bool);
       . ≤ . : (Real → Bool) × Real;
       . ≤ . : Real × (Real → Bool);
       bounded≥ : (Real → Bool);
   
   variables 
       r : Real;
       rset : Real → Bool;
       i : Int;
       j : Int;
   
   partial functions 
       sup : (Real → Bool) → Real with λ rset. bounded≤(rset);
       inf : (Real → Bool) → Real with λ rset. bounded≥(rset);
   
   
   axioms 
      boundedle-def: bounded≤(rset) ↔ (∃ r0. rset ≤ r0);
      used for: ls;
      
      boundedge-def: bounded≥(rset) ↔ (∃ r0. r0 ≤ rset);
      used for: ls;
      
      upperbound-def: rset ≤ r0 ↔ (∀ r. rset(r) → r ≤ r0);
      used for: ls;
      
      lowerbound-def: r0 ≤ rset ↔ (∀ r. rset(r) → r0 ≤ r);
      used for: ls;
      
      sup-exists: ∀ rset. bounded≤(rset) → (∃ r0. rset ≤ r0 ∧ (∀ r1. r1 < r0 → ¬ rset ≤ r1));
      
      sup-upperbound: bounded≤(rset) → rset ≤ sup(rset);
      used for: ss;
      
      sup-lowest-upperbound: bounded≤(rset) ∧ rset ≤ r → sup(rset) ≤ r;
      used for: ss;
      
      inf-lowerbound: bounded≥(rset) → inf(rset) ≤ rset;
      used for: ss;
      
      inf-highest-lowerbound: bounded≥(rset) ∧ r ≤ rset → r ≤ inf(rset);
      used for: ss;
   
   theorems 
      inf-exists: ∀ rset. bounded≥(rset) → (∃ r0. r0 ≤ rset ∧ (∀ r1. r0 < r1 → ¬ r1 ≤ rset));
      
      sup-unique: bounded≤(rset), rset ≤ r0 ∧ (∀ r1. r1 < r0 → ¬ rset ≤ r1), rset ≤ r ∧ (∀ r1. r1 < r → ¬ rset ≤ r1) ⊦ r0 = r;
      comment: justifies definition of sup as skolem function;
      
      inf-unique: bounded≥(rset), r0 ≤ rset ∧ (∀ r1. r0 < r1 → ¬ r1 ≤ rset), r ≤ rset ∧ (∀ r1. r < r1 → ¬ r1 ≤ rset) ⊦ r0 = r;
      comment: justifies definition of inf as skolem function;
   
   
end enrich