极限C^N（具有|c| <1）为0（伊莎贝尔）

Question

有谁知道表示

"¦c¦<1 ==> (λn. c^n) ---> 0" 

在实数

规则？

我发现使用“查询”面板以下规则：

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 

虽然我通过什么手段op有点困惑。

Answer 1

你试图证明的引理正好是LIMSEQ_rabs_realpow_zero2。因此你可以用apply (rule LIMSEQ_rabs_realpow_zero2)来证明你的目标。

E.g.请在伊莎贝尔尝试term "λx y. x + y"或term "λx. 1 + x"。输出将分别为op +和op + 1。

op ^只是λx y. x^y的简写。通常，Isabelle中的op是将二进制中缀运算符转换为具有两个参数（有点像ML中的一个）的函数的语法。