|
unif_cont_fun [ T : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%
% Additions made by Ricky W. Butler NASA Langley
%
%----------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING continuous_functions[T], convergence_sequences
f, f1, f2 : VAR [T -> real]
g : VAR [T -> nzreal]
u : VAR real
x, x0 : VAR T
epsi, delta : VAR posreal
%%% E : VAR { S : setof[real] | subset?(S, T_pred) }
E : VAR setof[T]
uniformly_continuous?(f, E) : bool =
FORALL (epsi: posreal): EXISTS (delta: posreal):
FORALL (x,y: (E)): abs(x-y) < delta IMPLIES
abs(f(x) - f(y)) < epsi
P3: VAR [real,real,posnat -> bool]
getem_scaf4: LEMMA (FORALL (n: posnat): EXISTS (x,y: real): P3(x,y,n))
IMPLIES (EXISTS (XX,YY: [posnat -> real]):
FORALL (k: posnat): P3(XX(k),YY(k),k))
a,b,c: VAR T
unif_cont_interval: LEMMA a < b IMPLIES
LET D = {xx:T | a <= xx AND xx <= b} IN
continuous_on?(f,D) IMPLIES
uniformly_continuous?(f,D)
END unif_cont_fun
¤ 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.
|
