c^n 的极限（¦c¦<1）为 0 (Isabelle)

Question

有谁知道显示规则

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

实数？

我使用 'query' 面板发现了以下规则：

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

来证明您的目标

例如在 Isabelle 中尝试 term "λx y. x + y" 或 term "λx. 1 + x"。输出将分别为 op + 和 op + 1。

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

c^n 的极限（¦c¦<1）为 0 (Isabelle)

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

isabelle

isar