|
%------------------------------------------------------------------------------
% Partitions
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Partitioning a set into a set of sets. Note pleasant combining function
% "join"
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
partitions[T:TYPE]: THEORY
BEGIN
a,a1,a2: VAR set[T]
A: VAR setofsets[T]
partition?(A,a):bool
= Union(A) = a AND FORALL (x,y:(A)): x /= y => disjoint?(x,y)
finite_partition?(A,a):bool = partition?(A,a) AND is_finite(A)
partition: TYPE+ = (LAMBDA A: partition?(A,fullset[T])) CONTAINING
singleton[set[T]](fullset[T])
finite_partition: TYPE+ = (LAMBDA A: finite_partition?(A,fullset[T]))
CONTAINING singleton[set[T]](fullset[T])
p1,p2: VAR finite_partition
IMPORTING finite_sets@finite_cross
join(p1,p2):finite_partition
= {a | EXISTS (a1:(p1),a2:(p2)): a = intersection(a1,a2)}
END partitions
¤ Dauer der Verarbeitung: 0.14 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.
|
