:: The de l'Hospital Theorem
:: by Ma{\l}gorzata Korolkiewicz
::
:: Copyright (c) 1992-2021 Association of Mizar Users

theorem :: L_HOSPIT:1
for f being PartFunc of REAL,REAL
for x0 being Real st f is_continuous_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds
f is_convergent_in x0
proof end;

theorem Th2: :: L_HOSPIT:2
for f being PartFunc of REAL,REAL
for x0, t being Real holds
( f is_right_convergent_in x0 & lim_right (f,x0) = t iff ( ( for r being Real st x0 < r holds
ex t being Real st
( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ () holds
( f /* a is convergent & lim (f /* a) = t ) ) ) )
proof end;

theorem Th3: :: L_HOSPIT:3
for f being PartFunc of REAL,REAL
for x0, t being Real holds
( f is_left_convergent_in x0 & lim_left (f,x0) = t iff ( ( for r being Real st r < x0 holds
ex t being Real st
( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ () holds
( f /* a is convergent & lim (f /* a) = t ) ) ) )
proof end;

theorem Th4: :: L_HOSPIT:4
for f being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st N \ {x0} c= dom f holds
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
proof end;

theorem :: L_HOSPIT:5
for f, g being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( N c= dom f & N c= dom g & f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f | N) / (g | N)) & f . x0 = 0 & g . x0 = 0 & (f | N) / (g | N) is_divergent_to+infty_in x0 ) holds
f / g is_divergent_to+infty_in x0
proof end;

theorem :: L_HOSPIT:6
for f, g being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( N c= dom f & N c= dom g & f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f | N) / (g | N)) & f . x0 = 0 & g . x0 = 0 & (f | N) / (g | N) is_divergent_to-infty_in x0 ) holds
f / g is_divergent_to-infty_in x0
proof end;

theorem :: L_HOSPIT:7
for f, g being PartFunc of REAL,REAL
for x0 being Real st x0 in (dom f) /\ (dom g) & ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f & [.x0,(x0 + r).] c= dom g & f is_differentiable_on ].x0,(x0 + r).[ & g is_differentiable_on ].x0,(x0 + r).[ & ].x0,(x0 + r).[ c= dom (f / g) & [.x0,(x0 + r).] c= dom ((f | ].x0,(x0 + r).[) / (g | ].x0,(x0 + r).[)) & f . x0 = 0 & g . x0 = 0 & f is_continuous_in x0 & g is_continuous_in x0 & (f | ].x0,(x0 + r).[) / (g | ].x0,(x0 + r).[) is_right_convergent_in x0 ) holds
( f / g is_right_convergent_in x0 & ex r being Real st
( r > 0 & lim_right ((f / g),x0) = lim_right (((f | ].x0,(x0 + r).[) / (g | ].x0,(x0 + r).[)),x0) ) )
proof end;

theorem :: L_HOSPIT:8
for f, g being PartFunc of REAL,REAL
for x0 being Real st x0 in (dom f) /\ (dom g) & ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f & [.(x0 - r),x0.] c= dom g & f is_differentiable_on ].(x0 - r),x0.[ & g is_differentiable_on ].(x0 - r),x0.[ & ].(x0 - r),x0.[ c= dom (f / g) & [.(x0 - r),x0.] c= dom ((f | ].(x0 - r),x0.[) / (g | ].(x0 - r),x0.[)) & f . x0 = 0 & g . x0 = 0 & f is_continuous_in x0 & g is_continuous_in x0 & (f | ].(x0 - r),x0.[) / (g | ].(x0 - r),x0.[) is_left_convergent_in x0 ) holds
( f / g is_left_convergent_in x0 & ex r being Real st
( r > 0 & lim_left ((f / g),x0) = lim_left (((f | ].(x0 - r),x0.[) / (g | ].(x0 - r),x0.[)),x0) ) )
proof end;

theorem :: L_HOSPIT:9
for f, g being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( N c= dom f & N c= dom g & f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f | N) / (g | N)) & f . x0 = 0 & g . x0 = 0 & (f | N) / (g | N) is_convergent_in x0 ) holds
( f / g is_convergent_in x0 & ex N being Neighbourhood of x0 st lim ((f / g),x0) = lim (((f | N) / (g | N)),x0) )
proof end;

:: l'Hospital Theorem
theorem :: L_HOSPIT:10
for f, g being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( N c= dom f & N c= dom g & f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f | N) / (g | N)) & f . x0 = 0 & g . x0 = 0 & (f | N) / (g | N) is_continuous_in x0 ) holds
( f / g is_convergent_in x0 & lim ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) )
proof end;