:: deftheorem Def3 defines left_improper_integral INTEGR24:def 3 :
for f being PartFunc of REAL,REAL
for a, b being Real st f is_left_improper_integrable_on a,b holds
for b₄ being ExtReal holds
( b₄ = left_improper_integral (f,a,b) iff ex Intf being PartFunc of REAL,REAL st
( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & ( ( Intf is_right_convergent_in a & b₄ = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & b₄ = +infty ) or ( Intf is_right_divergent_to-infty_in a & b₄ = -infty ) ) ) );