(* *)
(**************************************************************************)
-include "datatypes/subsets.ma".
+include "logic/equality.ma".
+include "logic/cprop_connectives.ma".
+
+record powerset (A : Type) : Type ≝ { char : A → CProp }.
+
+interpretation "char" 'subset p = (mk_powerset _ p).
+
+interpretation "pwset" 'powerset a = (powerset a).
+
+interpretation "in" 'mem a X = (char _ X a).
+
+definition subseteq ≝ λA.λu,v:\Omega \sup A.∀x.x ∈ u → x ∈ v.
+
+interpretation "subseteq" 'subseteq u v = (subseteq _ u v).
+
+definition overlaps ≝ λA.λU,V : Ω \sup A. exT2 ? (λx.x ∈ U) (λx.x ∈ V).
+
+interpretation "overlaps" 'overlaps u v = (overlaps _ u v).
+
+definition intersect ≝ λA.λu,v:Ω\sup A.{ y | y ∈ u ∧ y ∈ v }.
+
+interpretation "intersect" 'intersects u v = (intersect _ u v).
record axiom_set : Type ≝ {
A:> Type;
generalize in match H; clear H;
apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1);
clear H1; simplify; intros;
- [ exists [apply a1] assumption
+ [ exists [apply x] assumption
| cases H2 in j H H1; clear H2 a1; intros;
cases (H1 i); clear H1; apply (H3 a1); assumption]
qed.
-definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {b}.
+definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.
interpretation "covered by one" 'leq a b = (leq _ a b).
interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
+(*
record convergent_generated_topology : Type ≝
{ AA:> axiom_set;
- convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+ convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
}.
-
+*)