diff options
| author | Cyril Cohen | 2019-04-01 19:55:26 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-01 19:55:26 +0200 |
| commit | 9209c4414b22ead6b5a70d6f2bfb460b1ad26728 (patch) | |
| tree | b48d2702f2e5427683854d8f97b29c6948dad0d2 /mathcomp/ssreflect/binomial.v | |
| parent | 850862dc6475bd48524a294651400df4b5b7ecf3 (diff) | |
| parent | 0f785cb80a555ce4109255819becb953a968cc8c (diff) | |
Merge pull request #294 from math-comp/dependent-positive-finfun
Dependent positive finfun
Diffstat (limited to 'mathcomp/ssreflect/binomial.v')
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 1f0ae16..c99e296 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -365,10 +365,10 @@ Lemma card_inj_ffuns_on D T (R : pred T) : Proof. rewrite -card_uniq_tuples. have bijFF: {on (_ : pred _), bijective (@Finfun D T)}. - by exists val => // x _; apply: val_inj. -rewrite -(on_card_preimset (bijFF _)); apply: eq_card => t. -rewrite !inE -(codom_ffun (Finfun t)); congr (_ && _); apply: negb_inj. -by rewrite -has_predC has_map enumT has_filter -size_eq0 -cardE. + by exists fgraph => x _; [apply: FinfunK | apply: fgraphK]. +rewrite -(on_card_preimset (bijFF _)); apply: eq_card => /= t. +rewrite !inE -(big_andE predT) -big_filter big_all -all_map. +by rewrite -[injectiveb _]/(uniq _) [map _ _]codom_ffun FinfunK. Qed. Lemma card_inj_ffuns D T : |