feat(data/fintype/basic): The cardinality of a set is at most the car…

…dinality of the universe (#7823) I think that the hypothesis `[fintype ↥s]` can be avoided with the use of classical logic. E.g., `noncomputable instance set_fintype' {α : Type*} [fintype α] (s : set α) : fintype s :=by { classical, exact set_fintype s }` Would it make sense to add this? Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
leanprover-community · Jun 7, 2021 · 136e0d6 · 136e0d6
1 parent 4f38062
commit 136e0d6
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
@@ -947,9 +947,13 @@ instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fin
 fintype.subtype (univ.filter p) (by simp)
 
 /-- A set on a fintype, when coerced to a type, is a fintype. -/
-def set_fintype {α} [fintype α] (s : set α) [decidable_pred s] : fintype s :=
+def set_fintype {α} [fintype α] (s : set α) [decidable_pred (∈ s)] : fintype s :=
 subtype.fintype (λ x, x ∈ s)
 
+lemma set_fintype_card_le_univ {α : Type*} [fintype α] (s : set α) [fintype ↥s] :
+  fintype.card ↥s ≤ fintype.card α :=
+fintype.card_le_of_embedding (function.embedding.subtype s)
+
 namespace function.embedding
 
 /-- An embedding from a `fintype` to itself can be promoted to an equivalence. -/