Does anyone know a rule for showing
"¦c¦<1 ==> (λn. c^n) ---> 0"
in the reals?
I have found the following rules using the 'query' panel:
Limits.LIMSEQ_rabs_realpow_zero2: ¦?c¦ < 1 ⟹ op ^ ?c ---> 0
Limits.LIMSEQ_rabs_realpow_zero: ¦?c¦ < 1 ⟹ op ^ ¦?c¦ ---> 0
Limits.LIMSEQ_realpow_zero: 0 ≤ ?x ⟹ ?x < 1 ⟹ op ^ ?x ---> 0
although I am a little confused by what op means.
The lemma you are trying to prove is precisely LIMSEQ_rabs_realpow_zero2. You can therefore prove your goal with apply (rule LIMSEQ_rabs_realpow_zero2).
E.g. try term "λx y. x + y" or term "λx. 1 + x" in Isabelle. The output will be op + and op + 1, respectively.
The op ^ is simply a shorthand for λx y. x ^ y. In general, op in Isabelle is syntax for turning a binary infix operator into a function with two arguments (a bit like in ML).