Hi, suppose I have a function (f :num -> num -> real), and I want to calculate the sum of (f i j) on the entire plane, one way is to use double suminf: (assuming it is always summable, i.e. any sum is finite)
suminf (λi. suminf (λj. f i j))) (1) However, there’s another way using single suminf, based on numpairTheory: suminf (λn. f (nfst n) (nsnd n)) (2) My question is: how can I prove (1) and (2) are equal, i.e.: suminf (λi. suminf (λj. f i j))) = suminf (λn. f (nfst n) (nsnd n)) ? --Chun
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
