Coq 中连续的拓扑定义

Question

所以我对 coq 完全是函数式编程的新手，我正在尝试在 coq 中表达连续性的拓扑定义。我正在用这个 code 在 coq 中定义拓扑。我在给定特定函数的情况下表达连续性的最佳尝试是，

    Definition Continuous (X:Type)(TX:Topology X)(Y:Type)(TY:Topology Y)(f:X->Y):=
        forall V, exists U, all y:V, some x:U, f x = y.

我遇到错误

"The term "f x" has type "Y" while it is expected to have type "Prop".

不知道该怎么做，感谢您的帮助。

Answer 1

问题是 Coq 的解析器解释 y 错误。我可以通过稍微更改 all 和 some 的符号来解决问题：

Notation "'all' x 'in' U , P" := (forall x, U x -> P) (at level 200).
Notation "'some' x 'in' U , P" := (exists x, U x /\ P) (at level 200).

Definition continuous (X:Type)(TX:topology X)(Y:Type)(TY:topology Y)(f:X->Y):=
  forall V, exists U, all y in V, some x in U, f x = y.

注意符号级别有何不同以及它如何使用 in 关键字而不是 :。我不知道是否有办法让 : 工作；如果我尝试，Coq 8.5 一直抱怨。

Coq 中连续的拓扑定义

Topological Definition of Continuous in Coq

topology

coq