Skip to content
Snippets Groups Projects
Commit 60c6845c authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

coPset: some lemmas about infinity 

Proofs by Joshua Yanowski
parent b390cc24
No related branches found
No related tags found
1 merge request!230coPset: some lemmas about infinity
Pipeline #42961 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 7 additions and 0 deletions
theories/coPset.v
+ 7
− 0
View file @ 60c6845c
...@@ -453,3 +453,10 @@ Proof. ...@@ -453,3 +453,10 @@ Proof.
exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union, exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union,
coPset_lr_disjoint, coPset_l_finite, coPset_r_finite. coPset_lr_disjoint, coPset_l_finite, coPset_r_finite.
Qed. Qed.
Lemma coPset_split_infinite (X : coPset) :
set_infinite X →
∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ set_infinite X1 ∧ set_infinite X2.
Proof.
setoid_rewrite coPset_infinite_finite.
eapply coPset_split.
Qed.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment