Add is_Basisf_equiv.

Lebesgue/Set_theory/Set_system/Set_system_any.v

@@ -428,12 +428,26 @@ Context {U : Type}.
 
 Variable T : set_system U.
 
+Lemma is_Basisf_equiv :
+  forall {Idx : Type} (fB : Idx -> set U),
+    is_Basisf T fB <->
+    ((forall i, T (fB i)) /\
+     forall A x, T A -> A x -> exists i, incl (fB i) A /\ fB i x).
+Proof.
+intros; split; intros [HfB1 HfB2]; split; try easy.
+intros A x HA Hx; rewrite (HfB2 _ HA) in Hx;
+    destruct Hx as [i [Hi1 Hi2]]; exists i; easy.
+intros A HA; apply set_ext_equiv; split; intros x Hx.
+destruct (HfB2 _ _ HA Hx) as [i Hi]; exists i; easy.
+destruct Hx as [i [Hi1 Hi2]]; auto.
+Qed.
+
 Lemma is_Basisp_equiv :
   forall (PB : set_system U),
     is_Basisp T PB <->
     (Incl PB T /\ forall A x, T A -> A x -> exists B, PB B /\ incl B A /\ B x).
 Proof.
-intros PB; split; intros [HPB1 HPB2]; split; try easy.
+intros; split; intros [HPB1 HPB2]; split; try easy.
 intros A x HA Hx; rewrite (HPB2 _ HA) in Hx;
     destruct Hx as [B HB]; exists B; easy.
 intros A HA; apply set_ext_equiv; split; intros x Hx.
@@ -441,9 +455,9 @@ destruct (HPB2 _ _ HA Hx) as [B HB]; exists B; easy.
 destruct Hx as [B [[HB1 HB2] HB3]]; auto.
 Qed.
 
-Variable P : set_system U.
+Variable PB : set_system U.
 
-Lemma is_Basisp_Union_any_closure : is_Basisp (Union_any_closure P) P.
+Lemma is_Basisp_Union_any_closure : is_Basisp (Union_any_closure PB) PB.
 Proof.
 split.
 apply Union_any_closure_Gen.