:: deftheorem Def4 defines improper_integral_+infty INTEGR25:def 4 :
for f being PartFunc of REAL,REAL
for a being Real st f is_+infty_improper_integrable_on a holds
for b₃ being ExtReal holds
( b₃ = improper_integral_+infty (f,a) iff ex Intf being PartFunc of REAL,REAL st
( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) & ( ( Intf is convergent_in+infty & b₃ = lim_in+infty Intf ) or ( Intf is divergent_in+infty_to+infty & b₃ = +infty ) or ( Intf is divergent_in+infty_to-infty & b₃ = -infty ) ) ) );