Limit of c^n (with ¦c¦<1) is 0 (Isabelle)

Question

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.

Answer 1

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).