Topologische Definition von Continuous in Coq

Question

Also ich bin wirklich neu in Coq, funktionale Programmierung insgesamt, und ich versuche, die topologische Definition der Kontinuität in Coq auszudrücken. Ich verwende diese code, um eine Topologie in Coq zu definieren. Mein bester Versuch Kontinuität zum Ausdruck gegeben eine bestimmte Funktion ist,

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. 

Ich erhalte den Fehler

„Der Begriff‚fx‘hat Typ‚Y‘, während erwartet wird, Typ haben "Prop".

Keine Ahnung, was zu tun ist, jede Hilfe sehr geschätzt wird.

Answer 1

Das Problem ist, dass Coq Parserinterpretiertfalsch. Ich war in der Lage, das Problem zu beheben, indem Sie die Schreibweise für all und some ein wenig zu ändern:

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. 

Beachten Sie, wie die Notation Ebenen unterschiedlich sind und wie sie verwendet das in Schlüsselwort statt :. Ich weiß nicht, ob es einen Weg gibt, : zu funktionieren; Coq 8.5 beschwerte sich ständig, wenn ich es versuchte.