|
%------------------------------------------------------------------------------
% Topological Bases
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% The material presented here comes from Sutherland Chapter 3, Section 2
%
% Version 1.0 1/11/06 Initial Version
%------------------------------------------------------------------------------
basis[T:TYPE]: THEORY
BEGIN
IMPORTING topology_prelim[T]
t: VAR topology
U,V,W: VAR setofsets[T]
A: VAR set[T]
base?(t)(U):bool = subset?(U,t) AND
FORALL (A:(t)): EXISTS V: subset?(V,U) AND Union(V) = A
% Def 3.2.1
base?(t,U):bool = base?(t)(U)
synthetic_base?(U):bool
= (EXISTS V: subset?(V,U) AND Union(V) = fullset[T]) AND
FORALL (B1,B2:(U)): (EXISTS V: subset?(V,U) AND
Union(V) = intersection(B1,B2)) % Def 3.2.2
synthetic_base: TYPE = (synthetic_base?)
synthetic_base_is_setofsets: JUDGEMENT synthetic_base SUBTYPE_OF setofsets[T]
B: VAR synthetic_base
synthetic_generated_topology_set(B):setofsets[T]
= {A | EXISTS V: subset?(V,B) AND Union(V) = A}
synthetic_generated_def: LEMMA
member(A,synthetic_generated_topology_set(B)) IFF
EXISTS V: subset?(V,B) AND Union(V) = A
synthetic_generated_alt_def: LEMMA
member(A,synthetic_generated_topology_set(B)) IFF
A = Union({x:(B) | subset?(x,A)})
synthetic_generated_empty:
LEMMA member(emptyset[T],synthetic_generated_topology_set(B))
synthetic_generated_full:
LEMMA member(fullset[T],synthetic_generated_topology_set(B))
synthetic_generated_Union:
LEMMA topology_Union?(synthetic_generated_topology_set(B))
synthetic_generated_intersection:
LEMMA topology_intersection?(synthetic_generated_topology_set(B))
synthetic_generated_topology(B):topology
= {A | EXISTS V: subset?(V,B) AND Union(V) = A}
synthetic_basis_is_topology:
JUDGEMENT synthetic_generated_topology_set(B) HAS_TYPE topology
base_is_synthetic_base: LEMMA base?(t)(U) => synthetic_base?(U)
synthetic_base_is_base:
LEMMA base?(synthetic_generated_topology_set(B))(B)
subbase?(t)(U):bool
= subset?(U,t) AND
base?(t)({A | EXISTS V: is_finite(V) AND subset?(V,U) AND
A = Intersection(V)})
subbase?(t,U):bool = subbase?(t)(U)
synthetic_subbase?(U):bool
= synthetic_base?({A | EXISTS V: is_finite(V) AND subset?(V,U) AND
A = Intersection(V)})
synthetic_subbase: TYPE = (synthetic_subbase?)
synthetic_subbase_is_setofsets:
JUDGEMENT synthetic_subbase SUBTYPE_OF setofsets[T]
S: VAR synthetic_subbase
% synthetic_base_is_synthetic_subbase:
% JUDGEMENT synthetic_base SUBTYPE_OF synthetic_subbase
END basis
¤ Dauer der Verarbeitung: 0.13 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.
|
