Dear all,
I am working in HOL Light and I want to verify the following theorem
regarding integrability of a vector function:
*f integrable_on (:real^1) ==> f integrable_on {t | a <= drop t}*
which says that if a function is integrable on (-inf, inf) then it is
integrable on its subset which looks true to me.
Can anyone guide me in its proof?
Thanks.
--
Adnan
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
