From d7ac180f24b9c672c028d5bc2094059b4ba72178 Mon Sep 17 00:00:00 2001 From: Carl Friedrich Bolz-Tereick Date: Sat, 11 Jul 2020 10:11:11 +0000 Subject: [PATCH] feat(data/fintype/basic): set.to_finset_empty (#3361) Add set.to_finset_empty, analogously to set.to_finset_univ. --- src/data/fintype/basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean index 2cb1ffe71150f..832434c04f582 100644 --- a/src/data/fintype/basic.lean +++ b/src/data/fintype/basic.lean @@ -644,6 +644,10 @@ set_fintype _ (set.univ : set α).to_finset = finset.univ := by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] } +@[simp] lemma set.to_finset_empty [fintype α] : + (∅ : set α).to_finset = ∅ := +by { ext, simp only [set.mem_empty_eq, set.mem_to_finset, not_mem_empty] } + theorem fintype.card_subtype_le [fintype α] (p : α → Prop) [decidable_pred p] : fintype.card {x // p x} ≤ fintype.card α := by rw fintype.subtype_card; exact card_le_of_subset (subset_univ _)