|
%------------------------------------------------------------------------------
% Continuous Functions bewteen Scott Topologies
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990
%
% We give the Domain Theoretical formulation of Continuity
% (scott_continuous_def) and show that the pointwise order on functions is
% itself directed complete (pointwise_complete).
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 25/12/07 Initial Version
%------------------------------------------------------------------------------
scott_continuity[T1,T2:TYPE, (IMPORTING orders@directed_orders)
le1:(directed_complete_partial_order?[T1]),
le2:(directed_complete_partial_order?[T2])]: THEORY
BEGIN
IMPORTING scott[T1,le1], scott[T2,le2], fun_preds_partial[T1,T2,le1,le2],
topology@continuity_def[T1,scott_open_sets[T1,le1],
T2,scott_open_sets[T2,le2]],
topology@continuity[T1,scott_open_sets[T1,le1],
T2,scott_open_sets[T2,le2]]
D: VAR directed[T1,le1]
a: VAR T2
f: VAR [T1->T2]
g: VAR (increasing?)
% The following three Lemmata are D&P 3.15 (i)
lub_set_image: LEMMA lub_set?(image(g,D))
directed_image: LEMMA directed?[T2,le2](image(g,D))
lub_image: LEMMA le2(lub(image(g,D)),g(lub(D)))
% The following is D&P 3.15 (ii)
lub_image_increasing: LEMMA
(FORALL D: directed?[T2,le2](image(f,D)) AND
le2(lub[T2,le2](image(f,D)),f(lub[T1,le1](D))))
IMPLIES increasing?(f)
lub_preserving?(f):bool = FORALL D: lub_set?(image(f,D)) IMPLIES
f(lub(D)) = lub(image(f,D))
scott_continuous?(f):bool = increasing?(f) AND lub_preserving?(f)
scott_continuous: TYPE = (scott_continuous?)
scott_continuous_def: LEMMA continuous?(f) IFF scott_continuous?(f)
scott_continuous_is_continuous:
JUDGEMENT (scott_continuous?) SUBTYPE_OF (continuous?)
continuous_is_scott_continuous:
JUDGEMENT (continuous?) SUBTYPE_OF (scott_continuous?)
continuous_is_increasing:
JUDGEMENT (continuous?) SUBTYPE_OF (increasing?)
continuous_is_lub_preserving:
JUDGEMENT (continuous?) SUBTYPE_OF (lub_preserving?)
IMPORTING structures@const_fun_def[T1,T2],
topology@constant_continuity[T1,scott_open_sets[T1,le1],
T2,scott_open_sets[T2,le2]]
const_scott_continuous: JUDGEMENT const_fun(a) HAS_TYPE scott_continuous
IMPORTING orders@directed_orders[(scott_continuous?)],
orders@pointwise_orders[T1,T2]
pointwise_complete: LEMMA
directed_complete?[(scott_continuous?)](pointwise(le2))
scott_continuous_dcpo: LEMMA
directed_complete_partial_order?[(scott_continuous?)](pointwise(le2))
IMPORTING scott[(scott_continuous?),(pointwise(le2))]
END scott_continuity
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
