Zulip Chat Archive

Stream: Is there code for X?

Topic: Cardinality of quotient ≤


view this post on Zulip 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 _)

view this post on Zulip Johan Commelin (Mar 30 2021 at 15:33):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 α :=

view this post on Zulip Eric Wieser (Mar 30 2021 at 16:24):

I think f should be explicit to match the injective lemma

view this post on Zulip 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