:: deftheorem defines is_-infty_improper_integrable_on INTEGR25:def 1 :
for f being PartFunc of REAL,REAL
for b being Real holds
( f is_-infty_improper_integrable_on b iff ( ( for a being Real st a <= b holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st
( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & ( Intf is convergent_in-infty or Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) ) ) );