# Zulip Chat Archive

## 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 `apply`

ing this and then you'd want to fill in f

Last updated: May 07 2021 at 22:14 UTC