|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
