|
%------------------------------------------------------------------------------
% Linking metric continuity to that in analysis, for T from real.
%
% Author: David Lester, Manchester University
%
% Version 1.0 15/06/09 Initial Version
%------------------------------------------------------------------------------
continuity_link[T: TYPE FROM real]: THEORY
BEGIN
IMPORTING analysis@continuous_functions[T],
metric_space_def[real,(LAMBDA (x,y:real): abs(x-y))],
metric_space[real,(LAMBDA (x,y:real): abs(x-y))],
topology@continuity_subspace[real,metric_induced_topology,
real,metric_induced_topology,T],
metric_continuity[T,(lambda (x,y:T): abs(x-y)),
real,(LAMBDA (x,y:real): abs(x-y))]
f: VAR [T->real]
x: VAR T
continuous_iff_continuous_at?: LEMMA
continuous?[T](f,x) <=>
%RWB continuous_at?[T,induced_topology,real,metric_induced_topology](f,x)
continuous_at?[T, metric_induced_topology[T, (LAMBDA (x, y: T): abs(x - y))],
real,
metric_induced_topology
[real, (LAMBDA (x, y: real): abs(x - y))]](f,x)
continuous_iff_continuous?: LEMMA
continuous?[T](f) <=>
%RWB continuous?[T,induced_topology,real,metric_induced_topology](f)
continuous?[T, metric_induced_topology[T, (LAMBDA (x, y: T): abs(x - y))],
real, metric_induced_topology
[real, (LAMBDA (x, y: real): abs(x - y))]](f)
END continuity_link
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot
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
|
