WIP: parts of UniformSpace_compl.v will be moved to Topology.v (and use the Subset*.v API).

Lebesgue/UniformSpace_compl.v

@@ -76,6 +76,28 @@ apply filter_and; try assumption.
 apply (Hflim (fun x' => D x' -> P x') HP).
 Qed.
 
+Lemma open_not_equiv :
+  forall {T : UniformSpace} (A : T -> Prop),
+    open (fun x => ~ A x) <-> closed A.
+Proof.
+intros T A; split; try apply open_not.
+intros HA x; apply or_to_imply.
+destruct (imply_to_or _ _ (HA x)) as [Hx | Hx].
+right; apply NNPP; easy.
+left; easy.
+Qed.
+
+Lemma closed_not_equiv :
+  forall {T : UniformSpace} (A : T -> Prop),
+    closed (fun x => ~ A x) <-> open A.
+Proof.
+assert (H : forall T (A : T -> Prop), A = fun x => ~ ~ A x).
+  intros; apply functional_extensionality;
+      intros; apply propositional_extensionality; split; try easy; apply NNPP.
+intros T A; rewrite (H T A) at 1.
+rewrite open_not_equiv; easy.
+Qed.
+
 Lemma open_and_finite :
   forall {T : UniformSpace} (A : nat -> T -> Prop) N,
     (forall n, (n < S N)%nat -> open (A n)) ->
@@ -240,29 +262,17 @@ intros y [Hy1 Hy2]; split; [apply He1b | apply He2b];
     apply ball_le with e; try easy; [apply Rmin_l | apply Rmin_r].
 Qed.
 
-Lemma continuous_equiv_open :
+Lemma continuous_is_open_compat :
   forall {T1 T2 : UniformSpace} (f : T1 -> T2),
-    (forall x1, continuous f x1) <->
-    (forall A2, open A2 -> open (fun x1 => A2 (f x1))).
+    (forall x1, continuous f x1) ->
+    forall A2, open A2 -> open (fun x1 => A2 (f x1)).
 Proof.
-intros T1 T2 f; split; intros Hf.
-(* *)
-intros A2 HA2 x1 Hx1.
-admit.
-
-(* *)
-intros x1 A2 HA2.
+intros T1 T2 f Hf A2 HA2 x1 Hx1.
 
 
 
 
-Admitted.
 
-Lemma continuous_equiv_closed :
-  forall {T1 T2 : UniformSpace} (f : T1 -> T2),
-    (forall x1, continuous f x1) <->
-    (forall A2, closed A2 -> closed (fun x1 => A2 (f x1))).
-Proof.
 Admitted.
 
 End UniformSpace_compl.
@@ -298,98 +308,16 @@ Definition topo_basis_Prod : (nat -> T1 * T2 -> Prop) :=
 End topo_basis_Def.
 
 
-Section Subset_compl1.
-
-Context {U : Type}. (* Universe. *)
-
-Variable A : U -> Prop. (* Subset. *)
-
-Definition subset_to_Idx : {x | A x} -> U := proj1_sig (P := A).
-
-Lemma subset_to_Idx_correct : forall x, A x <-> exists i, x = subset_to_Idx i.
-Proof.
-intros x; split.
-intros Hx; exists (exist _ x Hx); easy.
-intros [[y Hy] Hx]; rewrite Hx; easy.
-Qed.
-
-Context {Idx : Type}. (* 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. *)
-
-Lemma subset_of_Idx_to_Idx :
-  forall (A : U -> Prop) x, subset_of_Idx (subset_to_Idx A) x <-> A x.
-Proof.
-intros A x; split.
-intros [[y Hy] Hi]; rewrite Hi; easy.
-intros Hx.
-assert (i : {x | A x}) by now exists x.
-exists i. (* Pb: i is no longer bound to x! *)
-
-Admitted.
-
-(* WIP: this one is not typing yet!
-Lemma subset_to_Idx_of_Idx :
-  forall Idx (B : Idx -> U) i, subset_to_Idx (subset_of_Idx B) i = B i.
-Proof.
-Admitted.
-*)
-
-End Subset_compl2.
-
-
-Section topo_basis_Facts.
+Section topo_basis_Facts1.
 
 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 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).
+Lemma is_topo_basis_Prop_open : is_topo_basis_Prop (@open T).
 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.
+split; try easy.
+intros A HA x; split.
+intros Hx; exists A; easy.
+intros [B [[HB1 HB2] HB3]]; auto.
 Qed.
 
 (* Still useful?
@@ -458,7 +386,7 @@ intros [B1 HB1] [B2 HB2]; exists (topo_basis_Prod B1 B2).
 apply topo_basis_Prod_correct; easy.
 Qed.
 
-End topo_basis_Facts.
+End topo_basis_Facts1.
 
 
 Section R_UniformSpace_compl.