From e88843ca30f8528899ef04aa0846604e078fdeb0 Mon Sep 17 00:00:00 2001 From: Joseph Myers Date: Sun, 30 Aug 2020 23:20:13 +0000 Subject: [PATCH] feat(data/finset/sort): range_mono_of_fin (#3987) Add a `simp` lemma giving the range of `mono_of_fin`. --- src/data/finset/sort.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/data/finset/sort.lean b/src/data/finset/sort.lean index 6cbd34e3c2fe8..33077058d30c9 100644 --- a/src/data/finset/sort.lean +++ b/src/data/finset/sort.lean @@ -154,6 +154,14 @@ end by rw [subsingleton.elim i ⟨0, zero_lt_one⟩, mono_of_fin_zero h (singleton_nonempty a) zero_lt_one, min'_singleton] +/-- The range of `mono_of_fin`. -/ +@[simp] lemma range_mono_of_fin {s : finset α} {k : ℕ} (h : s.card = k) : + set.range (s.mono_of_fin h) = ↑s := +begin + rw ←set.image_univ, + exact (mono_of_fin_bij_on s h).image_eq +end + /-- Any increasing bijection between `fin k` and a finset of cardinality `k` has to coincide with the increasing bijection `mono_of_fin s h`. For a statement assuming only that `f` maps `univ` to `s`, see `mono_of_fin_unique'`.-/