fix(data/fintype/basic): move card_subtype_mono into the fintype name…

…space (#15185)
leanprover-community · Jul 8, 2022 · 5a5d290 · 5a5d290
1 parent 1937dff
commit 5a5d290
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
@@ -1515,7 +1515,7 @@ begin
   intro; simp only [set.mem_to_finset, set.mem_compl_eq]; refl,
 end
 
-theorem card_subtype_mono (p q : α → Prop) (h : p ≤ q)
+theorem fintype.card_subtype_mono (p q : α → Prop) (h : p ≤ q)
   [fintype {x // p x}] [fintype {x // q x}] :
   fintype.card {x // p x} ≤ fintype.card {x // q x} :=
 fintype.card_le_of_embedding (subtype.imp_embedding _ _ h)