diff options
| author | Christian Doczkal | 2020-06-26 11:25:15 +0200 |
|---|---|---|
| committer | Christian Doczkal | 2020-06-26 11:25:15 +0200 |
| commit | a79e8b941cfd4a3343a90f14fba3b7f70293e679 (patch) | |
| tree | e99e0f620b040c187f5413f7a815ea4aceae1a80 | |
| parent | 3728862662bd0a5b836dfa746921954604d051ec (diff) | |
lemmas for proper and setC
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 9 |
2 files changed, 10 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 7a03f8e..935d165 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -19,7 +19,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `card_le1_eqP` (generalizes `fintype_le1P`), - in `finset.v`, neq lemmas: `set_enum`, `cards_eqP`, `cards2P` - in `fingraph.v`, new lemmas: `fcard_gt0P`, `fcard_gt1P` - +- in `finset.v`, new lemmas: `properC`, `properCr`, `properCl` ### Changed 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}. |