Add {open_or,closed_and}_any

WIP: alternative def of is_topo_basis.

Lebesgue/UniformSpace_compl.v

@@ -25,6 +25,7 @@ Section UniformSpace_compl.
 
 (** Complements on UniformSpace. **)
 
+(* Unused!
 Lemma filter_le_within_compat :
   forall {T : Type} {F G} (D : T -> Type),
     filter_le F G -> filter_le (within D F) (within D G).
@@ -32,7 +33,9 @@ Proof.
 intros T F G D HFG P H.
 now apply HFG.
 Qed.
+*)
 
+(* Unused!
 Lemma filterlim_locally_bis :
   forall {T : Type} {U : UniformSpace} {F} {FF : Filter F} (f : T -> U) y,
     filterlim f F (locally y) <->
@@ -50,6 +53,7 @@ apply filter_imp with (fun x => ball y eps (f x)).
 2: apply (H eps).
 intros x; apply Heps.
 Qed.
+*)
 
 Definition at_left_alt (x : R) : (R -> Prop) -> Prop :=
   within (fun x' => x' <= x) (locally x).
@@ -95,13 +99,20 @@ apply HN; intros; auto.
 auto.
 Qed.
 
+Lemma open_or_any :
+  forall {T : UniformSpace} {Idx : Type} (A : Idx -> T -> Prop),
+    (forall i, open (A i)) -> open (fun x => exists i, A i x).
+Proof.
+intros T Idx A HA x [i Hx].
+destruct (HA i x Hx) as [e He].
+exists e; intros; exists i; auto.
+Qed.
+
 Lemma open_or_count :
   forall {T : UniformSpace} (A : nat -> T -> Prop),
     (forall n, open (A n)) -> open (fun x => exists n, A n x).
 Proof.
-intros T A HA x [n Hx].
-destruct (HA n x Hx) as [e He].
-exists e; intros; exists n; auto.
+intro; apply open_or_any.
 Qed.
 
 Lemma open_or_finite :
@@ -144,14 +155,21 @@ intros Hx2; contradict Hx1; apply all_not_not_ex; intros n Hx3; apply (Hx2 n); e
 apply closed_not, open_and_finite; intros; apply open_not; auto.
 Qed.
 
+Lemma closed_and_any :
+  forall {T : UniformSpace} {Idx : Type} (A : Idx -> T -> Prop),
+    (forall i, closed (A i)) -> closed (fun x => forall i, A i x).
+Proof.
+intros T Idx A HA.
+apply closed_ext with (fun x => ~ exists i, ~ A i x).
+intros x; split; [apply not_ex_not_all | intros Hx1 [n Hx2]; auto].
+apply closed_not, open_or_any; intros; apply open_not; auto.
+Qed.
+
 Lemma closed_and_count :
   forall {T : UniformSpace} (A : nat -> T -> Prop),
     (forall n, closed (A n)) -> closed (fun x => forall n, A n x).
 Proof.
-intros T A HA.
-apply closed_ext with (fun x => ~ exists n, ~ A n x).
-intros x; split; [apply not_ex_not_all | intros Hx1 [n Hx2]; auto].
-apply closed_not, open_or_count; intros; apply open_not; auto.
+intro; apply closed_and_any.
 Qed.
 
 Lemma closed_and_finite :
@@ -227,6 +245,12 @@ End UniformSpace_compl.
 
 Section topo_basis_Def.
 
+Definition is_topo_basis_alt :
+    forall {T : UniformSpace}, ((T -> Prop) -> Prop) -> Prop :=
+  fun T PB =>
+    (forall B, PB B -> open B) /\
+    (forall A, open A -> forall x, A x <-> exists B, PB B /\ B x).
+
 Definition is_topo_basis :
     forall {T : UniformSpace} {Idx : Type}, (Idx -> T -> Prop) -> Prop :=
   fun T Idx B =>
@@ -251,6 +275,28 @@ End topo_basis_Def.
 
 Section topo_basis_Facts.
 
+Lemma is_topo_basis_correct :
+  forall {T : UniformSpace} {Idx : Type},
+    (exists (B : Idx-> T -> Prop), is_topo_basis B) <->
+    (exists (B : (T -> Prop) -> Prop), is_topo_basis_alt B).
+Proof.
+intros T Idx; split.
+(* *)
+intros [B [HB1 HB2]].
+exists (fun A => exists i, A = B i); split.
+intros A [i HA]; rewrite HA; auto.
+intros A HA x; destruct (HB2 A HA) as [P HP].
+rewrite HP; split.
+intros [i [Hi Hx]].
+
+
+
+
+
+
+
+Admitted.
+
 Lemma is_topo_basis_equiv :
   forall {T : UniformSpace} {Idx : Type} (B : Idx -> T -> Prop),
     (forall i, open (B i)) ->