4

在 Coq 中，我们可以通过定义如下lim类型的函数来形式化定义在 R 上的函数极限的概念：(R -> R) -> R -> R -> Prop

Require Import Coq.Reals.Reals.
Open Scope R.

Definition lim (f : R -> R) (c : R) (L : R) :=
  forall (eps : R), 0 < eps -> exists (del : R), 0 < del /\
  (forall (x : R), 0 < R_dist x c < del -> R_dist (f x) L < eps).

然后我们可以证明极限是唯一的：

Theorem lim_unique (f : R -> R) (c : R) (L M : R) :
  lim f c L -> lim f c M -> L = M.

但是在数学中，我们通常使用等号来写限制，例如“lim x->cf(x) = L”。这是因为限制的唯一性，所以 = 是等价关系的性质与我们在符号“lim x->cf(x) = L”中引入的 = 的这个新的隐式定义的含义兼容。

是否可以在 Coq 中以这种方式定义限制？更具体地说，我们可以定义一个函数lim2类型(R -> R) -> R -> R，使得lim2 f c = L当且仅当lim f c L？

4

0 回答 0