Stream: Beginner Questions

Topic: Does there exists a notion of $$A\times ...\times A$$?

Yiming Xu (Dec 02 2024 at 09:25):

I would like to talk about the product of n-copies of the same set. i.e. $A\times ...\times A$. I think this can be done with lists.

I can do something like:

definition n_fold_prod :: "nat ⇒ 'a set ⇒ 'a list set"
  where
"n_fold_prod n A = {as . length as = n ∧ (∀a. a ∈ set as ⟶ a ∈ A)}"

lemma finite_n_fold_prod :
  assumes "finite A"
  shows "finite (n_fold_prod n A)"

But I think it would be a common thing. Does it already exist somewhere?

Thanks!

Christian Pardillo Laursen (Dec 02 2024 at 10:33):

I think the standard way of doing this is PiE from FuncSet.thy
The product you're wanting is

abbreviation "n_fold_prod (n :: nat) A ≡ Pi⇩E {0..n} (λ_. A)"

lemma finite_n_fold_prod :
  assumes "finite A"
  shows "finite (n_fold_prod n A)"
  by (rule finite_PiE; simp add: assms)

Yiming Xu (Dec 02 2024 at 10:36):

Christian Pardillo Laursen said:

I think the standard way of doing this is PiE from FuncSet.thy
The product you're wanting is

abbreviation "n_fold_prod (n :: nat) A ≡ Pi⇩E {0..n} (λ_. A)"

lemma finite_n_fold_prod :
  assumes "finite A"
  shows "finite (n_fold_prod n A)"
  by (rule finite_PiE; simp add: assms)

Great! We even have indexed product in general. Thanks and lot and this is exactly what I want.

Last updated: Dec 21 2024 at 16:20 UTC