Finset.mem_pi
theorem Finset.mem_pi :
∀ {α : Type u_1} {β : α → Type u} [inst : DecidableEq α] {s : Finset α} {t : (a : α) → Finset (β a)}
{f : (a : α) → a ∈ s → β a}, f ∈ s.pi t ↔ ∀ (a : α) (h : a ∈ s), f a h ∈ t a
This theorem states that for any type `α`, function `β` from `α` to some other type, and for any set `s` of `α` and function `t` that maps each element of `α` to a set of `β a`, a function `f` is in the set of all functions (`Finset.pi s t`) defined on elements of `s` and taking values in `t a` for `a ∈ s`, if and only if for every element `a` in `s`, `f a h` is in the set `t a`. Here `f a h` retrieves the value of function `f` at point `a`, where `h` proves that `a` is in `s`. In short, function `f` is part of the product space `Finset.pi s t` if it assigns to each element of `s` a value in the corresponding `t a` set.
More concisely: A function `f` belongs to the product set `Finset.pi s t` if and only if `f a ∈ t a` for all `a ∈ s`.
|
Mathlib.Data.Finset.Pi._auxLemma.1
theorem Mathlib.Data.Finset.Pi._auxLemma.1 :
∀ {α : Type u_1} {β : α → Type u} [inst : DecidableEq α] {s : Finset α} {t : (a : α) → Finset (β a)}
{f : (a : α) → a ∈ s → β a}, (f ∈ s.pi t) = ∀ (a : α) (h : a ∈ s), f a h ∈ t a
This theorem states that for any type `α`, a function `β` from `α` to another type, a finite set `s` of `α`, and a function `t` mapping each element of `α` to a finite set of `β a`, if we have a function `f` that maps each element of `α` in `s` to `β a`, then `f` belongs to the set of all functions defined by `Finset.pi s t` if and only if for all elements `a` in `s`, the function `f` maps `a` to an element in `t a`. In other words, `f` is in the set produced by `Finset.pi` when `f` takes each element in `s` to an element in the corresponding set produced by `t`.
More concisely: For any type `α`, finite set `s` of `α`, function `t` mapping each `α` to a finite set of `β`, and function `f` from `s` to `β`, `f` is in the image of `Finset.pi s t` if and only if for all `a` in `s`, `f a` is in `t a`.
|