| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (PVS Prover Version 6.0.9©) Datei vom 28.9.2014 mit Größe 646 B |
|
Quelle sigma_fseq_def.pvsSprache: PVS |
|||||||||||||||
|
sigma_fseq_def[T: TYPE+ FROM real]: THEORY %------------------------------------------------------------------------------ % The summations theory provides properties of the sigma % function that sums up sequence of reals % % l(fs) % ---- % sigma(fs) = \ fs`seq(j) % / % ---- % j = 0 %------------------------------------------------------------------------------ BEGIN IMPORTING sigma_nat, structures@fseqs fs: VAR fseq[T] sigma(fs): real = sigma(0,l(fs)-1,(LAMBDA (n: nat): fs`seq(n))) END sigma_fseq_def
¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet am 2026-06-15) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09