:: deftheorem defines is_left_improper_integrable_on INTEGR24:def 1 :
for f being PartFunc of REAL,REAL
for a, b being Real holds
( f is_left_improper_integrable_on a,b iff ( ( for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) ) & 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 or Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) ) ) );