|
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
¤ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
