:: deftheorem Def3 defines improper_integral_-infty INTEGR25:def 3 :
for f being PartFunc of REAL,REAL
for b being Real st f is_-infty_improper_integrable_on b holds
for b₃ being ExtReal holds
( b₃ = improper_integral_-infty (f,b) iff 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 & 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 ) ) ) );