|
continuous_functions_more [ T : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%
% Additions made by Ricky W. Butler NASA Langley
%
%----------------------------------------------------------------------------
BEGIN
ASSUMING
connected_domain : ASSUMPTION
FORALL (x, y : T), (z : real) :
x <= z AND z <= y IMPLIES T_pred(z)
not_one_element : ASSUMPTION
FORALL (x : T) : EXISTS (y : T) : x /= y
ENDASSUMING
IMPORTING continuous_functions[T], convergence_sequences
f: VAR [T -> real]
a,b,c: VAR T
cn: VAR sequence[T]
n: VAR nat
convergence_fun_of : LEMMA convergence(cn,c) AND
continuous?(f,c) IMPLIES % move to analysis
convergence(LAMBDA n: f(cn(n)),f(c))
IMPORTING unif_cont_fun %% to maintain upward compatibility
END continuous_functions_more
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.5Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
