:: The de l'Hospital Theorem
:: by Ma{\l}gorzata Korolkiewicz
::
:: Received February 20, 1992
:: 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) /\ (right_open_halfline x0) 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) /\ (left_open_halfline x0) 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;