Cardinality of set of sets of integers with properties.

Stream: Is there code for X?

[Michail Karatarakis]

Hi, do we have this?

There are $(A+1)^n$ possible sets of integers $(x_1, \ldots, x_n)$ with $0 \leq x_k \leq A$ for $1 \leq k \leq n.$

example :
  let X : Set (Fin n → ℤ) := {x | ∀ (k : Fin n), 0 ≤ x k ∧ x k ≤ A}
  (Nat.card X) = (A + 1) ^ n := by sorry

[Yury G. Kudryashov]

You can build an equivalence with Fin n → Fin (A + 1).

[Yaël Dillies]

Just write your set as (Finset.univ : Finset (Fin n)).pi fun _ ↦ Icc (0 : ℤ) A and use docs#Finset.card_pi

[Michail Karatarakis]

I see, thanks. So, in general, I am dealing with finite sets with an increasingly number of conditions and I am not very familiar with the Finset API to generalize the stuff I am doing.

example {A B C : ℤ} : (Nat.card Y) ≤ (N*A*H + 1)^M := by
let Y := {y : Fin M → ℤ | ∀ j : Fin M, -B * H ≤ y ∧ y ≤ C * H ∧ B + C ≤ N * A};
  sorry

Furthermore, assuming I write the set below differently, how do I pull the elements out to prove trivial stuff like ? :

example {A : ℤ} :
  let X :=(Finset.univ : Finset (Fin n)).pi fun _ ↦ Icc (0 : ℤ) A;
     ↑(Nat.card ↑X) = (A + 1) ^ N →
            ∀ (finX : Finite ↑X),
                let hX := Fintype.ofFinite ↑X;
                    ∀ x ∈ Set.toFinset X,
                        ∀ (k : Fin N), |x k| ≤ A := by sorry

[Yaël Dillies]

Your set Y is ((Finset.univ : Finset (Fin M)).pi fun _ ↦ Icc (-B * H) (C * H)).filter fun _ ↦ B * C ≤ N * A (although it seems you have a typo somewhere since the filtering is trivial). For your second question, probably simp or aesop can do it.

[Peter Nelson]

I think this kind of thing indicates how difficult the Finset API is to work with for the uninitiated. Terms like attach and filter aren’t particularly intuitive.

[Yaël Dillies]

I agree. We need better notation.

[Yaël Dillies]

Better notation for s.filter p and univ.filter p would already go a long way.