diff options
| author | Cyril Cohen | 2020-08-11 02:49:27 +0200 |
|---|---|---|
| committer | GitHub | 2020-08-11 02:49:27 +0200 |
| commit | 16a8f48a4ac0a871ece84049f6271a6926e850e3 (patch) | |
| tree | 10aca5d616887d9e363b39722f44ef72d8743f9f /mathcomp | |
| parent | 0265476610747475a856f0560a86fe3b5409469f (diff) | |
| parent | a79e8b941cfd4a3343a90f14fba3b7f70293e679 (diff) | |
Merge pull request #541 from chdoc/properC
lemmas for proper and setC
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index f4c1dd5..9bd8c1f 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -639,6 +639,9 @@ Proof. by apply/setP=> x; rewrite !inE. Qed. Lemma setCT : ~: [set: T] = set0. Proof. by rewrite -setC0 setCK. Qed. +Lemma properC A B : (~: B \proper ~: A) = (A \proper B). +Proof. by rewrite !properE !setCS. Qed. + (* difference *) Lemma setDP A B x : reflect (x \in A /\ x \notin B) (x \in A :\: B). @@ -982,6 +985,12 @@ Qed. Lemma properD A B C : (A \proper B :\: C) -> (A \proper B) && [disjoint A & C]. Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed. +Lemma properCr A B : (A \proper ~: B) = (B \proper ~: A). +Proof. by rewrite -properC setCK. Qed. + +Lemma properCl A B : (~: A \proper B) = (~: B \proper A). +Proof. by rewrite -properC setCK. Qed. + End setOps. Arguments set1P {T x a}. |