:: The de l'Hospital Theorem
::  by Ma{\l}gorzata Korolkiewicz
::
:: Received February 20, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies PARTFUN1, NUMBERS, REAL_1, SEQ_1, SUBSET_1, FCONT_1, ARYTM_3,
      RELAT_1, LIMFUNC3, SEQ_2, ORDINAL2, TARSKI, XBOOLE_0, FUNCT_2, FUNCT_1,
      LIMFUNC2, LIMFUNC1, RCOMP_1, CARD_1, XXREAL_1, ARYTM_1, FDIFF_1,
      VALUED_1, XXREAL_0, NAT_1, ASYMPT_1, VALUED_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1,
      COMSEQ_2, SEQ_2, RELSET_1, PARTFUN1, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1,
      LIMFUNC1, LIMFUNC2, LIMFUNC3, XXREAL_0;
 constructors PARTFUN1, FUNCOP_1, REAL_1, NAT_1, SEQ_2, SEQM_3, PROB_1,
      RCOMP_1, RFUNCT_1, RFUNCT_2, FCONT_1, LIMFUNC1, FDIFF_1, LIMFUNC2,
      LIMFUNC3, VALUED_1, XXREAL_2, RELSET_1, SEQ_4, COMSEQ_2, SEQ_1;
 registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, RCOMP_1,
      VALUED_0, XXREAL_2, XBOOLE_0, SEQ_4, FUNCT_2, SEQ_1, SEQ_2;
 requirements SUBSET, ARITHM, NUMERALS;


begin

reserve f,g for PartFunc of REAL,REAL,
  r,r1,r2,g1,g2,g3,g4,g5,g6,x,x0,t,c for Real,
  a,b,s for Real_Sequence,
  n,k for Element of NAT;

theorem :: L_HOSPIT:1
  f is_continuous_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1
& g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_convergent_in
  x0;

theorem :: L_HOSPIT:2
  f is_right_convergent_in x0 & lim_right(f,x0) = t iff (for r st
x0<r ex t st t<r & x0<t & t in dom f) & for a 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;

theorem :: L_HOSPIT:3
  f is_left_convergent_in x0 & lim_left(f,x0) = t iff (for r st r<
  x0 ex t st r<t & t<x0 & t in dom f) & for a 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;

theorem :: L_HOSPIT:4
  (ex N being Neighbourhood of x0 st N\{x0} c=dom f) implies for r1
,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 &
  g2 in dom f;

theorem :: L_HOSPIT:5
  (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) implies f/g is_divergent_to+infty_in x0;

theorem :: L_HOSPIT:6
  (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) implies f/g is_divergent_to-infty_in x0;

theorem :: L_HOSPIT:7
  x0 in dom f /\ dom g & (ex r 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) implies f/g is_right_convergent_in x0 & ex r st r>0
  & lim_right(f/g,x0) = lim_right(((f`|(].x0,x0+r.[))/(g`|(].x0,x0+r.[))),x0);

theorem :: L_HOSPIT:8
  x0 in dom f /\ dom g & (ex r 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) implies f/g is_left_convergent_in x0 & ex r st r>0 &
  lim_left(f/g,x0) = lim_left(((f`|(].x0-r,x0.[))/(g`|(].x0-r,x0.[))),x0);

theorem :: L_HOSPIT:9
  (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) implies f/g is_convergent_in x0 & ex N being Neighbourhood of x0 st lim(f/g
  ,x0) = lim(((f`|N)/(g`|N)),x0);

::$N l'Hospital Theorem
theorem :: L_HOSPIT:10
  (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) implies f/g is_convergent_in x0 & lim(f/g,x0) = diff(f,x0)/diff(g,x0);