|
%------------------------------------------------------------------------------
% Properties of Continuous Functions between Scott Topologies
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990
%
% Extensions to orders@pointwise_orders.
% Note that pointwise ordering only preserves directed completeness for
% continuous functions.
%
% Version 1.0 25/12/07 Initial Version
%------------------------------------------------------------------------------
pointwise_orders_aux[T1,T2:TYPE]: THEORY
BEGIN
IMPORTING orders@pointwise_orders[T1,T2],
orders@directed_orders,
scott_continuity
d1: VAR (directed_complete_partial_order?[T1])
d2: VAR (directed_complete_partial_order?[T2])
p1: VAR (pointed_directed_complete_partial_order?[T1])
p2: VAR (pointed_directed_complete_partial_order?[T2])
continuous_pointwise(d1,d2)(f,g:scott_continuous[T1,T2,(d1),(d2)]):bool
= pointwise(d2)(f,g)
continuous_pointwise_preserves_directed_complete_partial_order: JUDGEMENT
continuous_pointwise(d1,d2) HAS_TYPE
(directed_complete_partial_order?[(scott_continuous?[T1,T2,(d1),(d2)])])
continuous_pointwise_preserves_pointed_directed_complete_partial_order:
JUDGEMENT
continuous_pointwise(p1,p2) HAS_TYPE
(pointed_directed_complete_partial_order?
[(scott_continuous?[T1,T2,(p1),(p2)])])
END pointwise_orders_aux
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
