feat(data/fintype): card_univ and card_univ_diff

leanprover-community · Mar 5, 2019 · 332121d · 332121d
1 parent c0b1eb1
commit 332121d
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/data/fintype.lean b/src/data/fintype.lean
@@ -190,6 +190,14 @@ def of_subsingleton (a : α) [subsingleton α] : fintype α :=
 
 end fintype
 
+lemma finset.card_univ [fintype α] : (finset.univ : finset α).card = fintype.card α :=
+rfl
+
+lemma finset.card_univ_diff [fintype α] [decidable_eq α] (s : finset α) :
+  (finset.univ \ s).card = fintype.card α - s.card :=
+eq.symm $ nat.sub_eq_of_eq_add $
+  by rw [← card_disjoint_union disjoint_sdiff, union_sdiff_of_subset (subset_univ _)]; refl
+
 instance (n : ℕ) : fintype (fin n) :=
 ⟨⟨list.pmap fin.mk (list.range n) (λ a, list.mem_range.1),
   list.nodup_pmap (λ a _ b _, congr_arg fin.val) (list.nodup_range _)⟩,