Skip to content
Snippets Groups Projects
Commit ab61ec0e authored by François Clément's avatar François Clément
Browse files

Use new result Union_any_inter_equiv.

WIP: add is_Open_Union_any_closure.
parent 58e56e3b
No related branches found
No related tags found
No related merge requests found
...@@ -464,16 +464,20 @@ rewrite full_equiv, HPB3; f_equal; set_ext_auto. ...@@ -464,16 +464,20 @@ rewrite full_equiv, HPB3; f_equal; set_ext_auto.
Qed. Qed.
Lemma is_Basisp_inter : Lemma is_Basisp_inter :
Inter T -> is_Basisp T PB -> Inter T -> is_Basisp T PB -> Union_any_inter PB.
forall B1 B2 x, PB B1 -> PB B2 -> inter B1 B2 x ->
exists B3, PB B3 /\ incl B3 (inter B1 B2) /\ B3 x.
Proof. Proof.
intros HT HPB B1 B2 x HB1 HB2 Hx. intros HT HPB; apply Union_any_inter_equiv; intros B1 B2 x HB1 HB2 Hx.
apply is_Basisp_equiv in HPB; destruct HPB as [HPB1 HPB2]. apply is_Basisp_equiv in HPB; destruct HPB as [HPB1 HPB2].
apply HPB2; try easy. apply HPB2; try easy.
apply HT; apply HPB1; easy. apply HT; apply HPB1; easy.
Qed. Qed.
Lemma is_Open_Union_any_closure :
full (unionp_any PB) -> Union_any_inter PB ->
is_Open (Union_any_closure PB).
Proof.
Admitted.
Lemma is_Basisp_Union_any_closure : is_Basisp (Union_any_closure PB) PB. Lemma is_Basisp_Union_any_closure : is_Basisp (Union_any_closure PB) PB.
Proof. Proof.
split. split.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment