let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st f is_Lcontinuous_in x0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) holds
( f is_left_convergent_in x0 & lim_left (f,x0) = f . x0 )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_Lcontinuous_in x0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) implies ( f is_left_convergent_in x0 & lim_left (f,x0) = f . x0 ) )
assume that
A1: f is_Lcontinuous_in x0 and
A2: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ; :: thesis: ( f is_left_convergent_in x0 & lim_left (f,x0) = f . x0 )
A3: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = f . x0 ) by A1, FDIFF_3:def 1;
hence f is_left_convergent_in x0 by A2, LIMFUNC2:def 1; :: thesis: lim_left (f,x0) = f . x0
hence lim_left (f,x0) = f . x0 by A3, LIMFUNC2:def 7; :: thesis: verum