|
%------------------------------------------------------------------------------
% Identity Function is Continuous
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 25/12/07 Initial Version
%------------------------------------------------------------------------------
scott_identity_continuity[T:TYPE,(IMPORTING orders@directed_orders[T])
le:(directed_complete_partial_order?)]: THEORY
BEGIN
IMPORTING scott_continuity[T,T,le,le],
topology@identity_continuity[T,scott_open_sets[T,le]]
id_scott_continuous: JUDGEMENT I[T] HAS_TYPE scott_continuous
END scott_identity_continuity
¤ Dauer der Verarbeitung: 0.18 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.
|
