極限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中的一個）的函數的語法。