Finset.pimage_eq_image_filter
theorem Finset.pimage_eq_image_filter :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
{s : Finset α},
Finset.pimage f s = Finset.image (fun x => (f ↑x).get ⋯) (Finset.filter (fun x => (f x).Dom) s).attach
This theorem states that for any types `α` and `β` with a decidable equality on `β`, any partially defined function `f` from `α` to `β`, a `s` being a finite set of `α`, and a decidable predicate on the domain of `f`, the image of `s` under `f` can be equivalently obtained by first filtering `s` to include only the elements for which `f` is defined, attaching the elements to their indices, and then applying `f` to the elements of the resulting set. The `fun x => (f ↑x).get ⋯` function is used to safely handle the partial function `f` by providing a default value when `f` is undefined.
More concisely: For any partially defined function `f` from type `α` to a type `β` with decidable equality, a finite set `s` of `α`, and a decidable predicate on the domain of `f`, the image of `s` under `f` is equal to the set obtained by filtering `s` to include only defined elements, attaching their indices as indices, and applying `f`.
|
Mathlib.Data.Finset.PImage._auxLemma.2
theorem Mathlib.Data.Finset.PImage._auxLemma.2 :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
{s : Finset α} {b : β}, (b ∈ Finset.pimage f s) = ∃ a ∈ s, b ∈ f a
This theorem states that for any types `α` and `β` with `β` having decidable equality, a partially defined function `f` from `α` to `β`, a finset `s` of `α`, and an element `b` of `β`, `b` belongs to the image of `s` under `f` if and only if there exists an element `a` in `s` such that `b` belongs to `f a`. Here, the image of `s` under `f` is defined as the finset of `β` obtained by applying `f` to each element of `s` and collecting the results into a finset. The existence of `b` in `f a` means that `f` is defined at `a` and `f a` equals `b`.
More concisely: For any partially defined function `f` from type `α` to decidably equal type `β`, and any finset `s` of `α` and element `b` of `β`, `b` is in the image of `s` under `f` if and only if there exists `a` in `s` such that `f a = b`.
|