:: deftheorem defines is_improper_integrable_on INTEGR24:def 5 :
for f being PartFunc of REAL,REAL
for a, c being Real holds
( f is_improper_integrable_on a,c iff ex b being Real st
( a < b & b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) & ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) ) );