cardinality of functions from Fin k

Stream: Is there code for X?

[chris477]

I’m having a hard time counting the number of possible values of a structure containing a function from Fun k under a certain condition. I have a Lemma that gives me a (finite) upper bound on the possible values for each function value under the condition. Since the type is not finite I’m using ENat.card and Set.encard. So essentially what I’m looking for is an extension of Set.encard_prod from pairs to arbitrary tuples. I had a look at Cardinality which might have it, but I’m a but lost in the notation and would appreciate any help! Thanks!

[Kevin Buzzard]

Can you post a #mwe ? This is the best way to ask questions on this forum.

[chris477]

Sure! We have in mathlib:

@[simp]
theorem ENat.card_prod (α β : Type*) : card (α × β) = card α * card β := by
  simp [ENat.card]

and I would like to extend this to arbitrary tuples of sets as follows (or rather use an existing lemma of course):

lemma card_fin_k_prod {k : ℕ} {α : Type*}
  (sets : Fin k → Set α) :
  ENat.card sets = ∏ i, ((sets i).encard) := by
  sorry

Here, lean complains that ENat.card is not applicable. I might also be confusing cardinality of types and cardinality of sets.

[Aaron Liu]

You have sets which is a k-tuple of subsets of α. You are trying to say that the cardinality of sets (which is a k-tuple) is equal to the product of the cardinalities of its components. Do you understand why that statement doesn't make sense?

[chris477]

Actually, in some way I understand it, in some way I don't. :D I think the issue comes from the fact that sometimes, ENat.card seems to be applied to values (when talking about the cardinality of a set) and sometimes it seems to be applied to types (when talking about the number of values that inhabit the type). But it might also be that my concept of a set is completely wrong.

But to maybe make some progress here, I think I can work with ENat.card_fun because the cardinalities can all be bounded by the same number in practice.

Thanks for your help!

[Aaron Liu]

chris477 said:

Actually, in some way I understand it, in some way I don't. :D I think the issue comes from the fact that sometimes, ENat.card seems to be applied to values (when talking about the cardinality of a set) and sometimes it seems to be applied to types (when talking about the number of values that inhabit the type).

That's because if you have a s : Set α and you put it in a place where it's expecting a type Lean does a coercion so that Set.Elem s is inserted there instead of s, and Set.Elem s is a type (the type of elements of s).

[chris477]

oh, I didn't expect that, thanks! Is that because of the @[coe] annotation of Elem?

[Aaron Liu]

the @[coe] annotation of Set.Elem only affects the pretty printer, so that you see ↑s instead of Set.Elem s in the pretty printer output. It's the instance that comes right after, which is docs#Set.instCoeSortType, that lets Lean find it as a coercion.

[chris477]

Nice, thanks!

[chris477]

Unfortunately, I'm still coming back to this issue. I was able to show

lemma card_fun {α : Type*} {k : ℕ} (S : Set (Fin k → α)) :
  { f : Fin k → α | ∀ i, ∃ s ∈ S, f i = s i}.encard ≤
    ∏ i, Cardinal.mk { x : α | ∃ s ∈ S, x = s i } := by

but not the corresponding lemma for encard, essentially because an analog of Cardinal.prod_eq_of_fintype is missing (and the fact that Set.encard can not be applied to tuples of sets).

Maybe another way to state the question would also be: The documentation in Data/Set/Card.lean explains the advantages and disadvantages of Set.encard, Set.ncard and Finset.card, but it does not mention Cardinal at all. I agree that Finset.card is super cumbersome to use if the type is not obviously finite, but should I rather work with Cardinal instead since it seems to have some lemmas that are missing from encard, or should encard be extended instead?

[chris477]

I created a pull request here for the encard version of the lemma: https://github.com/leanprover-community/mathlib4/pull/32644