|
%------------------------------------------------------------------------------
% Scott Topology
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990
%
% Notice that this is a T0 topology, and not Hausdorff (unless the order is
% equality).
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 25/12/07 Initial Version
%------------------------------------------------------------------------------
scott[T:TYPE, (IMPORTING orders@directed_orders[T])
<=:(directed_complete_partial_order?[T])]:THEORY
BEGIN
IMPORTING topology@topology_def[T],
orders@directed_order_props[T,<=]
x,y: VAR T
L: VAR lower_set
LS: VAR lower_sets
D: VAR directed
scott_closed_sets:setofsets[T]
= {L | FORALL D: subset?(D,L) IMPLIES member(lub(D),L)}
scott_open_sets:setofsets[T] = Complement(scott_closed_sets)
down_is_closed: LEMMA member(down(x),scott_closed_sets)
scott_empty: LEMMA member(emptyset, scott_closed_sets)
scott_full: LEMMA member(fullset, scott_closed_sets)
scott_union: LEMMA FORALL (A,B:(scott_closed_sets)):
member(union(A,B), scott_closed_sets)
scott_Intersection: LEMMA subset?(LS,scott_closed_sets) IMPLIES
member(Intersection(LS), scott_closed_sets)
scott_topology: LEMMA topology?(scott_open_sets)
scott_open_sets_is_topology: JUDGEMENT scott_open_sets HAS_TYPE topology
IMPORTING topology@topology[T,scott_open_sets]
A: VAR open_set
closed_is_lower: JUDGEMENT (closed?) SUBTYPE_OF lower_set
open_is_upper: JUDGEMENT (open?) SUBTYPE_OF upper_set
closure_is_down: LEMMA Cl(singleton(x)) = down(x)
order_iff_closure: LEMMA x <= y IFF member(x,Cl(singleton(y)))
order_iff_subset: LEMMA x <= y IFF FORALL A: member(x,A) IMPLIES member(y,A)
scott_is_T0: LEMMA T0_space?(scott_open_sets)
scott_hausdorff: LEMMA
hausdorff_space?(scott_open_sets) IFF trivial_partial_order?(<=)
END scott
¤ Dauer der Verarbeitung: 0.16 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.
|
