0

我已经定义了这样的拓扑空间，

Require Export Ensembles.
Arguments Full_set {U}.
Arguments Empty_set {U}.
Arguments In {U}.
Arguments Intersection {U}.
Arguments Union {U}.
Arguments Complement {U}.

Definition Family A := Ensemble (Ensemble A).
Inductive FamilyUnion {T : Type} (F: Family T) : Ensemble T :=
  | family_union_intro: forall (S:Ensemble T) (x:T),
      In F S -> In S x -> In (FamilyUnion F) x.

Inductive FamilyIntersection {T: Type} (F: Family T) : Ensemble T :=
  | family_intersect_intro : forall x, (forall (S:Ensemble T), (In F S) -> (In S x)) -> (In (FamilyIntersection F) x).

Record Topology : Type := mkTopology
{

          Point: Type;
          Open: Ensemble (Ensemble Point) ;
          EmptyOpen: (In Open Empty_set) ;
          FullOpen: (In Open Full_set) ;
          IntersectionOpen: forall x y,  (In Open x) -> (In Open y) -> (In Open (Intersection x y)) ;
          UnionOpen: forall F: (Family Point), (forall x: (Ensemble Point), (In F x) -> (In Open x)) -> In Open (FamilyUnion F)
}.


Definition Closed (T: Topology) := forall C: (Ensemble (Point T)),  In (Open T) (Complement C).

但当我试图定义时，

Theorem TopologyViaClosedSet {P: Type} (closed: Ensemble (Ensemble P)) 
    (emptyClosed: (In closed Empty_set)) 
    (fullClosed: (In closed Full_set)) 
    (unionClosed: (forall x y,  (In closed x) -> (In closed y) -> (In closed (Union x y)))) 
    (intersectionClosed: (forall F:(Family P), (forall x: (Ensemble P), (In F x) -> (In closed x)) -> (In closed (FamilyIntersection F)))) : 
    exists t: Topology,  forall x,  (In (Open t) x) <-> (In closed x)

它引发统一错误。我明白为什么它不能完成，但是我是否有可能暗示 Coq，里面的点字段不知何故t是P（(Point t) = P）？

4

1 回答 1

1

所以问题是，exists t : Topology, forall x : P, ...我们希望Point t在判断上等于P，它绑定得更远。我认为这是不可能的，所以我建议作为替代方案（您可能已经考虑过）：

  • 通过点字段索引拓扑，重新定义Topology为Topology (Point : Type)

  • 通过双射关联点场：exists (t : Topology) (f : P <-> Point Topology), forall x : P, In (Open t) (f x) <-> In closed x

于 2018-10-29T13:03:31.683 回答