Fix alternate representation of is_topo_basis.

Prove correctness results.

Lebesgue/UniformSpace_compl.v

@@ -245,18 +245,18 @@ 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 =>
     (forall i, open (B i)) /\
-    (forall (A : T -> Prop), open A ->
-      exists (P : Idx -> Prop), forall x, A x <-> exists i, P i /\ B i x).
+    (forall A, open A -> exists P, forall x, A x <-> exists i, P i /\ B i x).
+
+Definition is_topo_basis_Prop :
+    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 /\ forall y, B y -> A y) /\ B x).
 
 Definition is_second_countable : UniformSpace -> Prop :=
   fun T => exists (B : nat -> T -> Prop), is_topo_basis B.
@@ -273,37 +273,99 @@ Definition topo_basis_Prod : (nat -> T1 * T2 -> Prop) :=
 End topo_basis_Def.
 
 
-Section topo_basis_Facts.
+Section Subset_compl1.
+
+Context {U : Type}. (* Universe. *)
+
+Variable A : U -> Prop. (* Subset. *)
 
-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).
+Definition subset_to_Idx : {x | A x} -> U := @proj1_sig U A.
+
+Lemma subset_to_Idx_correct : forall x, A x <-> exists i, x = subset_to_Idx i.
 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]].
+intros x; split.
+intros Hx; exists (exist _ x Hx); easy.
+intros [[y Hy] Hx]; rewrite Hx; easy.
+Qed.
 
+Variable Idx : Type. (* Should be in Set? *) (* Indices. *)
+Variable B : Idx -> U.
 
+Definition subset_of_Idx : U -> Prop := fun x => exists i, x = B i.
 
+(* Useless?
+Lemma subset_of_Idx_correct :
+  forall x, (exists i, x = B i) <-> subset_of_Idx x.
+Proof.
+tauto.
+Qed.
+*)
+
+End Subset_compl1.
 
 
+Section Subset_compl2.
 
+Context {U : Type}. (* Universe. *)
 
+(* WIP...
+Lemma subset_of_Idx_to_Idx : forall A, subset_of_Idx (subset_to_Idx A) = A.
+Proof.
 Admitted.
 
+Lemma subset_to_Idx_of_Idx :
+  forall Idx (B : Idx -> U), subset_to_Idx (subset_of_Idx Idx B) = B.
+Proof.
+Admitted.
+*)
+
+End Subset_compl2.
+
+
+Section topo_basis_Facts.
+
+Context {T : UniformSpace}.
+
+Lemma is_topo_basis_to_Prop :
+  forall Idx (B : Idx -> T -> Prop),
+    is_topo_basis B -> is_topo_basis_Prop (subset_of_Idx Idx B).
+Proof.
+intros Idx B [HB1 HB2]; split.
+intros B' [i HB']; rewrite HB'; auto.
+intros A HA x; destruct (HB2 A HA) as [P HP]; rewrite HP; split.
+(* *)
+intros [i [Hi Hx]]; exists (B i); repeat split; try exists i; try easy.
+intros y Hy; apply <- HP; exists i; easy.
+(* *)
+intros [B' [[[i HB'1] HB'2] HB'3]].
+destruct (proj1 (HP x) (HB'2 x HB'3)) as [j Hj]; exists j; easy.
+Qed.
+
+Lemma is_topo_basis_of_Prop :
+  forall (PB : (T -> Prop) -> Prop),
+    is_topo_basis_Prop PB -> is_topo_basis (subset_to_Idx PB).
+Proof.
+intros PB [HPB1 HPB2]; split.
+intros i; apply HPB1, subset_to_Idx_correct; exists i; easy.
+intros A HA; exists (fun i => forall y, subset_to_Idx PB i y -> A y); intros x.
+rewrite (HPB2 _ HA); split.
+(* *)
+intros [B' [[HB'1 HB'2] HB'3]].
+destruct (proj1 (subset_to_Idx_correct PB B') HB'1) as [i Hi]; rewrite Hi in *.
+exists i; easy.
+(* *)
+intros [i [Hi1 Hi2]].
+exists (subset_to_Idx PB i); repeat split; try easy.
+apply subset_to_Idx_correct; exists i; easy.
+Qed.
+
+(* Still useful?
 Lemma is_topo_basis_equiv :
-  forall {T : UniformSpace} {Idx : Type} (B : Idx -> T -> Prop),
-    (forall i, open (B i)) ->
+  forall {Idx : Type} (B : Idx -> T -> Prop), (forall i, open (B i)) ->
     is_topo_basis B <->
     (forall A (x : T), open A -> A x -> exists i, B i x /\ forall y, B i y -> A y).
 Proof.
-intros T Idx B HB1; split; intros HB2.
+intros Idx B HB1; split; intros HB2.
 (* *)
 intros A x HA Hx.
 destruct (proj2 HB2 A HA) as [P HP]. destruct (proj1 (HP x) Hx) as [i [Hi1 Hi2]].
@@ -316,15 +378,18 @@ intros x; split.
 intros Hx; destruct (HB2 A x HA Hx) as [i [Hi1 Hi2]]; exists i; easy.
 intros [i [Hi1 Hi2]]; auto.
 Qed.
+*)
+
+Context {K1 K2 : AbsRing}.
+
+Let T1 := AbsRing_UniformSpace K1.
+Let T2 := AbsRing_UniformSpace K2.
 
 Lemma topo_basis_Prod_correct :
-  forall {K1 K2},
-    let T1 := AbsRing_UniformSpace K1 in
-    let T2 := AbsRing_UniformSpace K2 in
-    forall (B1 : nat -> T1 -> Prop) (B2 : nat -> T2 -> Prop),
-      is_topo_basis B1 -> is_topo_basis B2 -> is_topo_basis (topo_basis_Prod B1 B2).
+  forall (B1 : nat -> T1 -> Prop) (B2 : nat -> T2 -> Prop),
+    is_topo_basis B1 -> is_topo_basis B2 -> is_topo_basis (topo_basis_Prod B1 B2).
 Proof.
-intros K1 K2 T1 T2 B1 B2 [HB1a HB1b] [HB2a HB2b]; split.
+intros B1 B2 [HB1a HB1b] [HB2a HB2b]; split.
 (* *)
 intros; apply open_prod; auto.
 (* *)
@@ -353,14 +418,10 @@ intros [n [Hn1 Hn2]]; auto.
 Qed.
 
 Lemma is_second_countable_Prod :
-  forall {K1 K2},
-    let T1 := AbsRing_UniformSpace K1 in
-    let T2 := AbsRing_UniformSpace K2 in
-    is_second_countable T1 -> is_second_countable T2 ->
-    is_second_countable (prod_UniformSpace T1 T2).
-Proof.
-intros K1 K2 T1 T2 [B1 HB1] [B2 HB2].
-exists (topo_basis_Prod B1 B2).
+  is_second_countable T1 -> is_second_countable T2 ->
+  is_second_countable (prod_UniformSpace T1 T2).
+Proof.
+intros [B1 HB1] [B2 HB2]; exists (topo_basis_Prod B1 B2).
 apply topo_basis_Prod_correct; easy.
 Qed.