Basic definitions moved to Subset_system_def.v.

Lebesgue/Subset_system_base.v

@@ -18,90 +18,8 @@ From Coq Require Import ClassicalChoice.
 From Coq Require Import Arith Lia.
 
 Require Import logic_compl nat_compl.
-Require Import Subset Subset_finite Subset_seq.
-
-
-Section Subset_system_Prop_Def.
-
-Context {U : Type}. (* Universe. *)
-
-Variable P Q : (U -> Prop) -> Prop. (* Subset systems. *)
-
-Definition Incl : Prop := @incl (U -> Prop) P Q.
-
-Definition Same : Prop := @same (U -> Prop) P Q.
-
-End Subset_system_Prop_Def.
-
-
-Section Subset_system_Prop.
-
-Context {U : Type}. (* Universe. *)
-
-(** Extensionality of systems of subsets. *)
-
-Lemma Ext :
-  forall (P Q : (U -> Prop) -> Prop),
-    Same P Q -> P = Q.
-Proof.
-exact (@subset_ext (U -> Prop)).
-Qed.
-
-Lemma Ext_equiv :
-  forall (P Q : (U -> Prop) -> Prop),
-    P = Q <-> Incl P Q /\ Incl Q P.
-Proof.
-exact (@subset_ext_equiv (U -> Prop)).
-Qed.
-
-(** Incl is an order binary relation. *)
-
-Lemma Incl_refl :
-  forall (P Q : (U -> Prop) -> Prop),
-    Same P Q -> Incl P Q.
-Proof.
-exact (@incl_refl (U -> Prop)).
-Qed.
-
-Lemma Incl_antisym :
-  forall (P Q : (U -> Prop) -> Prop),
-    Incl P Q -> Incl Q P -> P = Q.
-Proof.
-exact (@incl_antisym (U -> Prop)).
-Qed.
-
-Lemma Incl_trans :
-  forall (P Q R : (U -> Prop) -> Prop),
-    Incl P Q -> Incl Q R -> Incl P R.
-Proof.
-exact (@incl_trans (U -> Prop)).
-Qed.
-
-(** Same is an equivalence binary relation. *)
-
-(* Useless?
-Lemma Same_refl :
-  forall (P : (U -> Prop) -> Prop),
-    Same P P.
-Proof.
-easy.
-Qed.*)
-
-Lemma Same_sym :
-  forall (P Q : (U -> Prop) -> Prop),
-    Same P Q -> Same Q P.
-Proof.
-exact (@same_sym (U -> Prop)).
-Qed.
-
-Lemma Same_trans :
-  forall (P Q R : (U -> Prop) -> Prop),
-    Same P Q -> Same Q R -> Same P R.
-Proof.
-exact (@same_trans (U -> Prop)).
-Qed.
-
-End Subset_system_Prop.
+Require Import Subset Subset_finite Subset_seq Subset_any Function.
+Require Import Subset_system_def.
 
 
 Section Base_Def.
@@ -1315,7 +1233,6 @@ Qed.
 End Seq_Facts1.
 
 
-(* WIP.
 Section Seq_Facts2.
 
 (** More facts about properties of subset systems involving countable operations. *)
@@ -1335,33 +1252,32 @@ Lemma Inter_Union_disj_seq_closure :
   Inter P -> Inter (Union_disj_seq_closure P).
 Proof.
 intros H A A' [B [HB1 HB2]] [B' [HB'1 HB'2]].
-Aglopted.
+Admitted.
 
 Lemma Inter_seq_Union_disj_seq_closure :
   Inter P -> Inter_seq (Union_disj_seq_closure P).
 Proof.
-Aglopted.
+Admitted.
 
 Lemma Union_disj_Union_disj_seq_closure :
   Union_disj (Union_disj_seq_closure P).
 Proof.
 intros A A' H [B [HB1 HB2]] [B' [HB'1 HB'2]].
 (* Use mix? *)
-Aglopted.
+Admitted.
 
 Lemma Union_disj_seq_Union_disj_seq_closure :
   Union_disj_seq (Union_disj_seq_closure P).
 Proof.
-Aglopted.
+Admitted.
 
 Lemma Diff_Union_disj_seq_closure :
   Inter P -> Part_diff_seq P -> Diff (Union_disj_seq_closure P).
 Proof.
 intros H1 H2 A A' [B [HB1 [HB2 HB3]]] [B' [HB'1 [HB'2 HB'3]]].
-Aglopted.
+Admitted.
 
 End Seq_Facts2.
-*)
 
 
 Section Trace_Facts2.
@@ -1396,12 +1312,20 @@ Variable P : (U -> Prop) -> Prop. (* Subset system. *)
 
 Definition Inter_any : Prop :=
   forall (A : Idx -> U -> Prop),
-    (forall idx, P (A idx)) ->
-    P (fun x => forall idx, A idx x).
+    (forall i, P (A i)) ->
+    P (inter_any A).
 
 Definition Union_any : Prop :=
   forall (A : Idx -> U -> Prop),
-    (forall idx, P (A idx)) ->
-    P (fun x => exists idx, A idx x).
+    (forall i, P (A i)) ->
+    P (union_any A).
+
+Definition Inter_Prop : Prop :=
+  forall (PA : (U -> Prop) -> Prop),
+    Incl PA P -> P (inter_Prop PA).
+
+Definition Union_Prop : Prop :=
+  forall (PA : (U -> Prop) -> Prop),
+    Incl PA P -> P (union_Prop PA).
 
 End Any_Def.