| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/scott/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle pointwise_orders_aux.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% 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.8 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28