# Image of a Finset α under a partially defined function #

In this file we define Part.toFinset and Finset.pimage. We also prove some trivial lemmas about these definitions.

## Tags #

finite set, image, partial function

def Part.toFinset {α : Type u_1} (o : Part α) [Decidable o.Dom] :

Convert an o : Part α with decidable Part.Dom o to Finset α.

Equations
• o.toFinset = o.toOption.toFinset
Instances For
@[simp]
theorem Part.mem_toFinset {α : Type u_1} {o : Part α} [Decidable o.Dom] {x : α} :
x o.toFinset x o
@[simp]
theorem Part.toFinset_none {α : Type u_1} [Decidable Part.none.Dom] :
Part.none.toFinset =
@[simp]
theorem Part.toFinset_some {α : Type u_1} {a : α} [Decidable ().Dom] :
().toFinset = {a}
@[simp]
theorem Part.coe_toFinset {α : Type u_1} (o : Part α) [Decidable o.Dom] :
o.toFinset = {x : α | x o}
def Finset.pimage {α : Type u_1} {β : Type u_2} [] (f : α →. β) [(x : α) → Decidable (f x).Dom] (s : ) :

Image of s : Finset α under a partially defined function f : α →. β.

Equations
• = s.biUnion fun (x : α) => (f x).toFinset
Instances For
@[simp]
theorem Finset.mem_pimage {α : Type u_1} {β : Type u_2} [] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : } {b : β} :
b as, b f a
@[simp]
theorem Finset.coe_pimage {α : Type u_1} {β : Type u_2} [] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : } :
() = f.image s
@[simp]
theorem Finset.pimage_some {α : Type u_1} {β : Type u_2} [] (s : ) (f : αβ) [(x : α) → Decidable (Part.some (f x)).Dom] :
Finset.pimage (fun (x : α) => Part.some (f x)) s =
theorem Finset.pimage_congr {α : Type u_1} {β : Type u_2} [] {f : α →. β} {g : α →. β} [(x : α) → Decidable (f x).Dom] [(x : α) → Decidable (g x).Dom] {s : } {t : } (h₁ : s = t) (h₂ : xt, f x = g x) :
=
theorem Finset.pimage_eq_image_filter {α : Type u_1} {β : Type u_2} [] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : } :
= Finset.image (fun (x : { x : α // x Finset.filter (fun (x : α) => (f x).Dom) s }) => (f x).get ) (Finset.filter (fun (x : α) => (f x).Dom) s).attach

Rewrite s.pimage f in terms of Finset.filter, Finset.attach, and Finset.image.

theorem Finset.pimage_union {α : Type u_1} {β : Type u_2} [] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : } {t : } [] :
@[simp]
theorem Finset.pimage_empty {α : Type u_1} {β : Type u_2} [] {f : α →. β} [(x : α) → Decidable (f x).Dom] :
theorem Finset.pimage_subset {α : Type u_1} {β : Type u_2} [] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : } {t : } :
t xs, yf x, y t
theorem Finset.pimage_mono {α : Type u_1} {β : Type u_2} [] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : } {t : } (h : s t) :
theorem Finset.pimage_inter {α : Type u_1} {β : Type u_2} [] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : } {t : } [] :