|
%------------------------------------------------------------------------------
% Subspace Continuity
%
% Continuity is preserved on subspaces
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 8/10/04 Initial Version
% Version 1.1 9/06/06 Changed interface, added Type Judgements
%------------------------------------------------------------------------------
continuity_subspace[T1:TYPE, (IMPORTING topology_def[T1]) S:topology[T1],
T2:TYPE, (IMPORTING topology_def[T2]) T:topology[T2],
T3:TYPE FROM T1]: THEORY
BEGIN
IMPORTING subspace[T1,S,T3],
continuity[T1,S,T2,T],
continuity
x: VAR T3
f: VAR [T1->T2]
subspace_continuous_at: LEMMA continuous_at?(f,x) =>
continuous_at?[T3,induced_topology,T2,T](restrict[T1,T3,T2](f),x)
subspace_continuous: LEMMA continuous?(f) =>
continuous?[T3,induced_topology,T2,T](restrict[T1,T3,T2](f))
F: VAR continuous[T1,S,T2,T]
restrict_is_continuous:
JUDGEMENT restrict[T1,T3,T2](F) HAS_TYPE
continuous[T3,induced_topology,T2,T]
END continuity_subspace
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
