| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis/ (NIST Fortran ©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle real_fun_supinf.pvs Sprache: PVS |
|||||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Sup and Inf of bounded functions % % (require nonempty domain) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% real_fun_supinf [ T : NONEMPTY_TYPE FROM real ] : THEORY BEGIN IMPORTING reals@real_fun_props, reals@real_facts f : VAR [T -> real] x : VAR T a : VAR real epsilon : VAR posreal %--------------- % Sup and Inf %--------------- g : VAR { f | bounded_above?(f) } h : VAR { f | bounded_below?(f) } nonempty_image: JUDGEMENT Im(f) HAS_TYPE (nonempty?[real]) bounded_above_image: JUDGEMENT Im(g) HAS_TYPE (bounded_above?) bounded_below_image: JUDGEMENT Im(h) HAS_TYPE (bounded_below?) sup(g) : real = lub(Im(g)) inf(h) : real = glb(Im(h)) %-------------- % Properties %-------------- supfun_is_bound : LEMMA g(x) <= sup(g) supfun_is_sup : LEMMA FORALL epsilon : EXISTS x : sup(g) - epsilon < g(x) supfun_is_sup2 : LEMMA sup(g) <= a IFF FORALL x : g(x) <= a inffun_is_bound : LEMMA inf(h) <= h(x) inffun_is_inf : LEMMA FORALL epsilon : EXISTS x : h(x) < inf(h) + epsilon inffun_is_inf2 : LEMMA a <= inf(h) IFF FORALL x : a <= h(x) supfun_neg : LEMMA sup(- h) = - inf(h) inffun_neg : LEMMA inf(- g) = - sup(g) %-------------------------------------- % Relations with maximum and minimum %-------------------------------------- max_upper_bound : LEMMA is_maximum(x, f) IFF bounded_above?(f) AND sup(f) = f(x) min_lower_bound : LEMMA is_minimum(x, f) IFF bounded_below?(f) AND inf(f) = f(x) END real_fun_supinf ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28