| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/scott/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 789 B |
|
Quellcode-Bibliothek scott_identity_continuity.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% 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 ¤ 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.0.10Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
