Cardinality of quotient ≤

Stream: Is there code for X?

[Adrián Doña Mateo]

I am surprised these are not in mathlib already. Are they just formulated in a different way and I missed them?

import data.fintype.basic

open fintype

variables {α β : Type*} [fintype α] [fintype β]

lemma card_ge_of_surjective {f : α → β} (hf : function.surjective f) : card α ≥ card β :=
card_le_of_injective (function.surj_inv hf) (function.injective_surj_inv hf)

lemma card_quotient_le {s : setoid α} [decidable_rel s.r] :
  fintype.card (quotient s) ≤ fintype.card α :=
card_ge_of_surjective (surjective_quotient_mk _)

[Johan Commelin]

You can try library_search. Note that mathlib would flip the inequality to use \le

[Adrián Doña Mateo]

library_search doesn't seem to find anything, even flipping the inequality. I guess they really aren't there. In the second one, would it be preferable to have [s : setoid α] instead of an implicit argument?

[Mario Carneiro]

I don't think I did this one when setting up the theory, so it's probably a hole

[Adrián Doña Mateo]

In that case, I think it's worth adding them. To be mathlib-compliant, the first should flip the inequality, right? So instead:

lemma card_le_of_surjective {f : α → β} (hf : function.surjective f) : card β ≤ card α :=

[Eric Wieser]

I think f should be explicit to match the injective lemma

[Kevin Buzzard]

Right -- you can imagine applying this and then you'd want to fill in f