:: deftheorem defines is_improper_integrable_on_REAL INTEGR25:def 5 :
for f being PartFunc of REAL,REAL holds
( f is_improper_integrable_on_REAL iff ex r being Real st
( f is_-infty_improper_integrable_on r & f is_+infty_improper_integrable_on r & ( not improper_integral_-infty (f,r) = -infty or not improper_integral_+infty (f,r) = +infty ) & ( not improper_integral_-infty (f,r) = +infty or not improper_integral_+infty (f,r) = -infty ) ) );