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