From 559ba5831013fe28fe0ed18c2f5edef0d4887020 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Wed, 22 Jun 2022 13:59:18 +0200
Subject: [PATCH] Add is_Basisf_equiv.
---
.../Set_theory/Set_system/Set_system_any.v | 20 ++++++++++++++++---
1 file changed, 17 insertions(+), 3 deletions(-)
diff --git a/Lebesgue/Set_theory/Set_system/Set_system_any.v b/Lebesgue/Set_theory/Set_system/Set_system_any.v
index 3805f98e..9ea033b1 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_any.v
+++ b/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.
--
GitLab