diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 14 |
2 files changed, 17 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index dbe39cd..fb9381f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -32,7 +32,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`, - `existsPn`, `exists_inPn`, `forallPn`, `forall_inPn`. + `existsPn`, `exists_inPn`, `forallPn`, `forall_inPn`, + `eq_enum_rank_in`, `enum_rank_in_inj`, `lshift_inj`, and + `rshift_inj`. - Bigop theorems: `big_rmcond`, `bigD1_seq`, `big_enum_val_cond`, `big_enum_rank_cond`, diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index ffdf0a5..b6f618d 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -1831,6 +1831,14 @@ move=> Ax0; exists (enum_rank_in Ax0) => [i _|]; last exact: enum_rankK_in. exact: enum_valK_in. Qed. +Lemma eq_enum_rank_in (x0 y0 : T) A (Ax0 : x0 \in A) (Ay0 : y0 \in A) : + {in A, enum_rank_in Ax0 =1 enum_rank_in Ay0}. +Proof. by move=> x xA; apply: enum_val_inj; rewrite !enum_rankK_in. Qed. + +Lemma enum_rank_in_inj (x0 y0 : T) A (Ax0 : x0 \in A) (Ay0 : y0 \in A) : + {in A &, forall x y, enum_rank_in Ax0 x = enum_rank_in Ay0 y -> x = y}. +Proof. by move=> x y xA yA /(congr1 enum_val); rewrite !enum_rankK_in. Qed. + Lemma enum_rank_bij : bijective enum_rank. Proof. by move: enum_rankK enum_valK; exists (@enum_val T). Qed. @@ -2003,6 +2011,12 @@ Proof. by rewrite ltn_add2l. Qed. Definition lshift m n (i : 'I_m) := Ordinal (lshift_subproof n i). Definition rshift m n (i : 'I_n) := Ordinal (rshift_subproof m i). +Lemma lshift_inj m n : injective (@lshift m n). +Proof. by move=> ? ? /(f_equal val) /= /val_inj. Qed. + +Lemma rshift_inj m n : injective (@rshift m n). +Proof. by move=> ? ? /(f_equal val) /addnI /val_inj. Qed. + Lemma split_subproof m n (i : 'I_(m + n)) : i >= m -> i - m < n. Proof. by move/subSn <-; rewrite leq_subLR. Qed. |