|
%------------------------------------------------------------------------------
% Connected Spaces Definition
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
% Version 1.0 1/11/06 Initial Version
%------------------------------------------------------------------------------
connected_def[T:TYPE]: THEORY
BEGIN
IMPORTING topology_prelim[T],
topology_prelim[bool],
topology,
continuity_def,
continuity
U: VAR topology[T]
f: VAR (surjective?[T,bool])
connected_def: LEMMA connected?(U) IFF
FORALL (A,B:(U)): nonempty?(A) AND nonempty?(B) =>
NOT (disjoint?(A,B) AND Union(U) = union(A,B))
connected_def2: LEMMA connected?(U) IFF
FORALL f: NOT continuous?[T,(U),bool,discrete_topology[bool]](f)
END connected_def
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
