"Неявное" определение предела функции в Coq
В Coq мы можем формализовать понятие предела функции, определенной на R, определив функцию lim типа (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->c f(x) = L". Это работает из-за уникальности пределов, поэтому свойство = быть отношением эквивалентности совместимо с этим новым неявно определенным значением =, которое мы вводим в обозначении "lim x->c f(x) = L".
Можно ли таким образом определить пределы в Coq? Более конкретно, можем ли мы определить функцию lim2 типа (R -> R) -> R -> R такой, что lim2 f c = L если и только если lim f c L?