## Stream: Is there code for X?

### Topic: Cardinality of quotient ≤

#### Adrián Doña Mateo (Mar 30 2021 at 15:15):

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 (Mar 30 2021 at 15:33):

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

#### Adrián Doña Mateo (Mar 30 2021 at 15:39):

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 (Mar 30 2021 at 16:13):

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

#### Adrián Doña Mateo (Mar 30 2021 at 16:24):

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 (Mar 30 2021 at 16:24):

I think f should be explicit to match the injective lemma

#### Kevin Buzzard (Mar 30 2021 at 18:20):

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

Last updated: May 07 2021 at 22:14 UTC