Fix proof of {Inter,Union}_any_closure_is_Open.

Lebesgue/Set_theory/Set_system/Set_system_any.v

@@ -185,17 +185,13 @@ Qed.
 
 Lemma Union_any_closure_is_Open :
   forall (P : set_system U),
-    unionp_any P = fullset -> Union_any_inter P ->
+    full (unionp_any P) -> Union_any_inter P ->
     is_Open (Union_any_closure P).
 Proof.
-intros P HP1 HP2.
-assert (HP3 : wEmpty (Union_any_closure P)) by apply Union_any_closure_wEmpty.
-assert (HP4 : Union_any (Union_any_closure P))
-    by apply Union_any_closure_Union_any.
-apply is_Open_equiv; repeat split; try easy.
-unfold wFull; rewrite <- HP1; easy.
-apply Union_any_closure_Inter.
-
+intros; apply is_Open_equiv; repeat split.
+apply Union_any_closure_wEmpty.
+apply Union_any_closure_wFull; easy.
+apply Union_any_closure_Inter; easy.
 apply Union_any_closure_Unionf_any.
 Qed.
 
@@ -267,14 +263,14 @@ Qed.
 
 Lemma Inter_any_closure_is_Closed :
   forall (P : set_system U),
-    interp_any P = emptyset -> Inter_any_union P ->
+    empty (interp_any P) -> Inter_any_union P ->
     is_Closed (Inter_any_closure P).
 Proof.
-intros P HP1 HP2; apply is_Closed_equiv; repeat split.
-unfold wEmpty; rewrite <- HP1; easy.
-unfold wFull; rewrite <- interp_any_nullary; easy.
-apply Union_Inter_any_closure; easy.
-apply Interf_any_Inter_any_closure.
+intros; apply is_Closed_equiv; repeat split.
+apply Inter_any_closure_wEmpty; easy.
+apply Inter_any_closure_wFull.
+apply Inter_any_closure_Union; easy.
+apply Inter_any_closure_Interf_any.
 Qed.
 
 End Closed_Facts.
@@ -354,7 +350,7 @@ Lemma is_Open_is_Closed_complp_any_equiv :
 Proof.
 intros; rewrite is_Open_equiv, is_Closed_equiv.
 rewrite <- wFull_wEmpty_complp_any, <- wEmpty_wFull_complp_any,
-    <- Inter_Union_complp_any, <- Unionf_any_Interf_any_complp_any; easy.
+    <- Inter_Union_complp_any, Interf_any_complp_any_equiv; easy.
 Qed.
 
 Lemma is_Closed_is_Open_complp_any_equiv :
@@ -363,22 +359,6 @@ Proof.
 rewrite is_Open_is_Closed_complp_any_equiv, complp_any_invol; easy.
 Qed.
 
-Lemma is_Open_Union_any_closure :
-  full (unionp_any P) -> Union_any_inter P ->
-  is_Open (Union_any_closure P).
-Proof.
-intros HP1 HP2.
-assert (HP3 : wEmpty (Union_any_closure P)) by apply Union_any_closure_wEmpty.
-assert (HP4 : Union_any (Union_any_closure_U)
-
-
- apply is_Open_equiv; repeat split.
-apply Union_any_closure_wEmpty.
-apply Union_any_closure_wFull; easy.
-apply Union_any_closure_Inter.
-
-Admitted.
-
 End Set_system_Facts5.