Fintype.piFinset_image
theorem Fintype.piFinset_image :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {γ : α → Type u_2} {δ : α → Type u_3}
[inst_2 : (a : α) → DecidableEq (δ a)] (f : (a : α) → γ a → δ a) (s : (a : α) → Finset (γ a)),
(Fintype.piFinset fun a => Finset.image (f a) (s a)) = Finset.image (fun b a => f a (b a)) (Fintype.piFinset s)
The theorem `Fintype.piFinset_image` states that for every type `α` with decidable equality and finiteness, and for every pair of type functions `γ` and `δ` from `α` where each `δ a` also has decidable equality, given a function `f` mapping an element of `α` and `γ a` to `δ a`, and a function `s` mapping each `a` in `α` to a `Finset` of `γ a`, the image under `f` of the Cartesian product finset of `s a` across all `a` in `α` is equal to the Cartesian product finset of the image under `f` of `s a` for each `a` in `α`. In mathematical terms, this can be interpreted as distributing the image function across the Cartesian product of finsets.
More concisely: For every type `α` with decidable equality and finiteness, and for every pair of type functions `γ : α → Type* δ : α → Type` with decidable equality, given functions `f : α × γ → δ` and `s : α → Finset γ`, the image of the Cartesian product of `s a` under `f` for all `a` in `α` is equal to the Cartesian product of the images of `s a` under `f` for each `a` in `α`.
|
Mathlib.Data.Fintype.Pi._auxLemma.1
theorem Mathlib.Data.Fintype.Pi._auxLemma.1 :
∀ {α : Sort u_1} {β : α → Sort u} {f₁ f₂ : (x : α) → β x}, (f₁ = f₂) = ∀ (a : α), f₁ a = f₂ a
This theorem from the Mathlib Data.Fintype.Pi module states that for any types `α` and `β` (where `β` is a function from `α`), and for any two functions `f₁` and `f₂` from `α` to `β`, the equality of `f₁` and `f₂` is equivalent to the equality of `f₁ a` and `f₂ a` for all `a` in `α`. In other words, two functions are considered equal if they produce the same output for every input from the domain.
More concisely: For functions `f₁` and `f₂` from type `α` to type `β`, `f₁ = f₂` if and only if `∀ a ∈ α, f₁ a = f₂ a`.
|
Fintype.mem_piFinset
theorem Fintype.mem_piFinset :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_3} {t : (a : α) → Finset (δ a)}
{f : (a : α) → δ a}, f ∈ Fintype.piFinset t ↔ ∀ (a : α), f a ∈ t a
The theorem `Fintype.mem_piFinset` states that for all types `α` with decidable equality and finite cardinality, and for any function `δ` from `α` to another type, given a function `t` that assigns to each element of `α` a finite set of elements of the type given by `δ` for that element, and another function `f` from `α` to the type given by `δ`, the function `f` is a member of the finite product set `Fintype.piFinset t` if and only if for all elements of `α`, the output of `f` for that element is a member of the finite set given by `t` for that element.
More concisely: For any type `α` with decidable equality and finite cardinality, function `δ : α → Type`, function `t : α → Finset (δ α)`, and function `f : α → δ α`, `f ∈ ∏ x ∈ α. Finset (δ x)` if and only if `∀ x ∈ α, f x ∈ t x`.
|
Mathlib.Data.Fintype.Pi._auxLemma.9
theorem Mathlib.Data.Fintype.Pi._auxLemma.9 :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_3} {t : (a : α) → Finset (δ a)}
{f : (a : α) → δ a}, (f ∈ Fintype.piFinset t) = ∀ (a : α), f a ∈ t a
This theorem, `Mathlib.Data.Fintype.Pi._auxLemma.9`, states that for any type `α` that has decidable equality and is finite, for any function `δ` from `α` to another type `u_3`, for any function `t` from `α` to a `Finset` (a finite set) of `u_3` type, and for any function `f` from `α` to `u_3`, the condition that `f` is an element of the pi-Finset of `t` (i.e., the set of functions from `α` to `u_3` that send each element of `α` to an element in the corresponding `Finset` in `u_3`) is equivalent to the condition that for all elements `a` of `α`, `f(a)` is an element of `t(a)`.
In simpler terms, a function is in the pi-Finset of `t` if and only if it maps every element to a member of the corresponding set specified by `t`.
More concisely: For a finite type `α` with decidable equality, a function `δ : α → u_3`, a function `t : α → Finset u_3`, and a function `f : α → u_3`, `f` is in the pi-Finset of `t` if and only if `f(a) ∈ t(a)` for all `a : α`.
|