Quellcode-Bibliothek lim_of_composition.pvs   Sprache: PVS

lim_of_composition [ T1, T2 : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%  Author:  Bruno Dutertre    Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN

  IMPORTING lim_of_functions, continuous_functions[T2]

  f : VAR [T1 -> T2]
  g : VAR [T2 -> real]

  x, y : VAR real
  z : VAR T2

  l : VAR real


  adherence_lemma  : LEMMA convergence(f, x, y) 
                             IMPLIES adh[T2](fullset[real])(y)
        
  adherence_lemma2 : LEMMA convergent?(f, x) 
                             IMPLIES adh[T2](fullset[real])(lim(f, x))


  convergence_composition : LEMMA convergence(f, x, y) AND convergence(g, y, l)
                             IMPLIES convergence(g o f, x, l)

  convergent_composition  : LEMMA convergent?(f, x) AND convergent?(g, lim(f, x))
                             IMPLIES convergent?(g o f, x)

  lim_composition         : LEMMA convergent?(f, x) AND convergent?(g, lim(f, x))
                             IMPLIES lim(g o f, x) = lim(g, lim(f, x))


  convergence_comp_continuous: LEMMA convergence(f, x, z) AND continuous?(g, z) 
                                 IMPLIES convergence(g o f, x, g(z))

  convergent_comp_continuous : LEMMA convergent?(f, x) AND T2_pred(lim(f, x))
                              AND continuous?(g, lim(f, x))
                                 IMPLIES convergent?(g o f, x)

  lim_comp_continuous        : LEMMA convergent?(f, x) AND T2_pred(lim(f, x))
                              AND continuous?(g, lim(f, x))
                              IMPLIES
                                   lim(g o f, x) = g(lim(f, x))

END lim_of_composition