Renaming + cleaning (of doubles and useless results).

Mv def of continuity (to Set_system_def_any).

Lebesgue/Set_theory/Set_system/Topology.v

@@ -16,12 +16,12 @@ COPYING file for more details.
 
 (** General topology - bases and continuity (definitions and properties).
 
-  Generators of topologies are also called subbase, or prebase. *)
+  Generators of topologies are also called subbases, or prebases. *)
 
 Require Import Set_system.
 
 
-Section Basis_Facts3.
+Section Basis_Facts1.
 
 Context {U : Type}.
 Variable T : set_system U.
@@ -29,77 +29,36 @@ Variable PB : set_system U.
 Hypothesis HT : is_Open T.
 Hypothesis HPB : is_Basisp T PB.
 
+Lemma Basisp_full_unionp_any : full (unionp_any PB).
+Proof.
+apply is_Basisp_wFull with T; try apply is_Open_equiv; easy.
+Qed.
+
+Lemma Basisp_Union_any_inter : Union_any_inter PB.
+Proof.
+apply is_Basisp_Inter with T; try apply is_Open_equiv; easy.
+Qed.
+
 Lemma Basisp_is_gen : T = Open PB.
 Proof.
 destruct HPB as [HPB1 HPB2]; rewrite <- HT; apply Open_ext.
 (* *)
 intros A HA; rewrite (HPB2 _ HA).
-pose (PB_A := fun B => PB B /\ incl B A); fold PB_A.
-destruct (empty_dec PB_A) as [H | H].
+destruct (empty_dec (Subset A PB)) as [H | H].
 (* . *)
 rewrite empty_equiv in H; rewrite H, unionp_any_nullary.
 apply Open_wEmpty.
 (* . *)
 apply Open_Union_any; try easy.
-unfold PB_A; intros B HB; apply Open_Gen; easy.
+intros B HB; induction HB; apply Open_Gen; easy.
 (* *)
 intros B HB; apply Open_Gen; auto.
 Qed.
 
-Lemma Basisp_fullset : unionp_any PB = fullset.
-Proof.
-rewrite <- full_equiv; apply is_Basisp_wFull with T; try easy.
-apply is_Open_equiv; easy.
-Qed.
+End Basis_Facts1.
 
-Lemma Basisp_Union_any_inter : Union_any_inter PB.
-Proof.
-apply is_Basisp_Inter with T; try easy.
-apply is_Open_equiv; easy.
-Qed.
-
-End Basis_Facts3.
-
-
-Section Basis_Facts4.
-
-Context {U Idx : Type}.
-Variable T : set_system U.
 
-(* Note that the following results do not need T to be a topology! *)
-
-Lemma all_is_Basisf : is_Basisf T (skolem T).
-Proof.
-split.
-intros [x Hx]; easy.
-intros A HA; apply set_ext_equiv; split; intros x.
-intros; exists (exist _ _ HA); easy.
-intros [[B HB1] [HB2 HB3]]; auto.
-Qed.
-
-Lemma all_is_Basisp : is_Basisp T T.
-Proof.
-split; try easy.
-intros A HA; apply set_ext_equiv; split; intros x Hx.
-exists A; easy.
-destruct Hx as [B [[HB1 HB2] HB3]]; auto.
-Qed.
-
-Variable fB : Idx -> set U.
-
-(* Useful? *)
-Lemma Basisf_to_Basisp : is_Basisf T fB -> is_Basisp T (unskolem fB).
-Proof.
-apply (proj1 (is_Basisf_is_Basisp_equiv _ _)).
-Qed.
-
-Variable PB : set_system U.
-
-(* Useful? *)
-Lemma Basisf_of_Basisp : is_Basisp T PB -> is_Basisf T (skolem PB).
-Proof.
-apply (proj1 (is_Basisp_is_Basisf_equiv _ _)).
-Qed.
+Section Basis_Facts2.
 
 Context {U1 U2 : Type}.
 Variable T1 : set_system U1.
@@ -115,10 +74,10 @@ apply Incl_trans with (Preimage f T2); try easy.
 apply Preimage_monot; easy.
 Qed.
 
-End Basis_Facts4.
+End Basis_Facts2.
 
 
-Section Basis_Facts5.
+Section Basis_Facts3.
 
 Context {U1 U2 Idx1 Idx2 : Type}.
 Variable T1 : set_system U1.
@@ -162,27 +121,25 @@ intros [i [Hx1 Hx2]]; auto.
 *)
 Admitted.
 
-End Basis_Facts5.
+End Basis_Facts3.
 
 
-Section Continuous_Def.
+Section Continuous_fun_Facts1.
 
 Context {U1 U2 : Type}. (* Universes. *)
 Variable genU1 : set_system U1. (* Generator, or subbase. *)
 Variable genU2 : set_system U2. (* Generator, or subbase. *)
 
-Definition continuous_fun : set (U1 -> U2) :=
-  fun f => Incl (Preimage f (Open genU2)) (Open genU1).
-
 Lemma continuous_fun_ext :
-  forall f g, same_fun f g -> continuous_fun f -> continuous_fun g.
+  forall f g, same_fun f g ->
+    continuous_fun genU1 genU2 f -> continuous_fun genU1 genU2 g.
 Proof.
 intros f g H Hf _ [A2 HA2].
 rewrite <- (preimage_ext_fun f); try easy; apply Hf; easy.
 Qed.
 
 Lemma continuous_fun_equiv :
-  forall f, continuous_fun f <-> Incl (Preimage f genU2) (Open genU1).
+  forall f, continuous_fun genU1 genU2 f <-> Incl (Preimage f genU2) (Open genU1).
 Proof.
 intros f; split; intros Hf.
 intros _ [A2 HA2]; apply Hf, Im, Open_Gen; easy.
@@ -194,10 +151,10 @@ apply Open_Inter_finite; easy.
 apply Open_Unionf_any; easy.
 Qed.
 
-End Continuous_Def.
+End Continuous_fun_Facts1.
 
 
-Section Continuous_Facts1.
+Section Continuous_fun_Facts2.
 
 Context {U1 U2 : Type}.
 Variable genU1 : set_system U1.
@@ -223,7 +180,7 @@ split; intros Hf A1 HA1; induction HA1 as [A2 HA2].
 
 Admitted.
 
-End Continuous_Facts1.
+End Continuous_fun_Facts2.
 
 
 (* TODO: add section(s) on UniformSpace.