Module docstring
{"# Pointwise operations with lists of sets
This file proves some lemmas about pointwise algebraic operations with lists of sets. "}
Set.mem_prod_list_ofFn
theorem
{a : α} {s : Fin n → Set α} : a ∈ (List.ofFn s).prod ↔ ∃ f : ∀ i : Fin n, s i, (List.ofFn fun i ↦ (f i : α)).prod = a
Full source
@[to_additive]
theorem mem_prod_list_ofFn {a : α} {s : Fin n → Set α} :
a ∈ (List.ofFn s).proda ∈ (List.ofFn s).prod ↔ ∃ f : ∀ i : Fin n, s i, (List.ofFn fun i ↦ (f i : α)).prod = a := by
induction' n with n ih generalizing a
· simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
· simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ,
mem_mul, @ih, exists_exists_eq_and, SetCoe.exists, exists_prop]Informal description
For an element $a$ of type $\alpha$ and a family of sets $s_i$ indexed by $\text{Fin} n$, the element $a$ belongs to the product of the list of sets $(s_0, \dots, s_{n-1})$ if and only if there exists a function $f$ such that for each $i \in \text{Fin} n$, $f(i) \in s_i$, and the product of the list $(f(0), \dots, f(n-1))$ equals $a$.
Set.mem_list_prod
theorem
{l : List (Set α)} {a : α} :
a ∈ l.prod ↔ ∃ l' : List (Σ s : Set α, ↥s), List.prod (l'.map fun x ↦ (Sigma.snd x : α)) = a ∧ l'.map Sigma.fst = l
Full source
@[to_additive]
theorem mem_list_prod {l : List (Set α)} {a : α} :
a ∈ l.proda ∈ l.prod ↔
∃ l' : List (Σs : Set α, ↥s),
List.prod (l'.map fun x ↦ (Sigma.snd x : α)) = a ∧ l'.map Sigma.fst = l := by
induction' l using List.ofFnRec with n f
simp only [mem_prod_list_ofFn, List.exists_iff_exists_tuple, List.map_ofFn, Function.comp,
List.ofFn_inj', Sigma.mk.inj_iff, and_left_comm, exists_and_left, exists_eq_left, heq_eq_eq]
constructor
· rintro ⟨fi, rfl⟩
exact ⟨fun i ↦ ⟨_, fi i⟩, rfl, rfl⟩
· rintro ⟨fi, rfl, rfl⟩
exact ⟨fun i ↦ _, rfl⟩Informal description
For a list of sets $l$ over a type $\alpha$ and an element $a \in \alpha$, $a$ belongs to the product of the sets in $l$ if and only if there exists a list $l'$ of pairs $(s, x)$ where $s \in l$ and $x \in s$, such that the product of the elements $x$ in $l'$ equals $a$ and the list of first components of $l'$ equals $l$.
In symbols:
$$
a \in \prod l \leftrightarrow \exists l' : \text{List}(\Sigma s \in l, s), \quad \prod_{(s, x) \in l'} x = a \ \land \ \text{map } \sigma_1 l' = l
$$
Set.mem_pow
theorem
{a : α} {n : ℕ} : a ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i ↦ (f i : α)).prod = a
Full source
@[to_additive]
theorem mem_pow {a : α} {n : ℕ} :
a ∈ s ^ na ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i ↦ (f i : α)).prod = a := by
rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]Informal description
For an element $a$ of type $\alpha$, a natural number $n$, and a set $s \subseteq \alpha$, the element $a$ belongs to the $n$-th power set $s^n$ (under the monoid operation) if and only if there exists a function $f : \text{Fin } n \to s$ such that the product of the list $(f(0), \dots, f(n-1))$ equals $a$.
In symbols:
$$
a \in s^n \leftrightarrow \exists f : \text{Fin } n \to s, \quad \prod_{i=0}^{n-1} f(i) = a
$$