From 60c6845c141dd94368d09388326cfc9f035f82f4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Mar 2021 18:08:04 +0100
Subject: [PATCH] coPset: some lemmas about infinity
Proofs by Joshua Yanowski
---
theories/coPset.v | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/theories/coPset.v b/theories/coPset.v
index e86d831d..8e8cb978 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -453,3 +453,10 @@ Proof.
exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union,
coPset_lr_disjoint, coPset_l_finite, coPset_r_finite.
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.
--
GitLab