# mathlib3documentation

data.finset.pimage

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define part.to_finset and finset.pimage. We also prove some trivial lemmas about these definitions.

## Tags #

finite set, image, partial function

def part.to_finset {α : Type u_1} (o : part α) [decidable o.dom] :

Convert a o : part α with decidable part.dom o to finset α.

Equations
@[simp]
theorem part.mem_to_finset {α : Type u_1} {o : part α} [decidable o.dom] {x : α} :
@[simp]
theorem part.to_finset_none {α : Type u_1}  :
@[simp]
theorem part.to_finset_some {α : Type u_1} {a : α} [decidable (part.some a).dom] :
@[simp]
theorem part.coe_to_finset {α : Type u_1} (o : part α) [decidable o.dom] :
(o.to_finset) = {x : α | x o}
def finset.pimage {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α →. β) [Π (x : α), decidable (f x).dom] (s : finset α) :

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

Equations
@[simp]
theorem finset.mem_pimage {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s : finset α} {b : β} :
b (a : α) (H : a s), b f a
@[simp, norm_cast]
theorem finset.coe_pimage {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s : finset α} :
s) = f.image s
@[simp]
theorem finset.pimage_some {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (f : α β) [Π (x : α), decidable (part.some (f x)).dom] :
finset.pimage (λ (x : α), part.some (f x)) s = s
theorem finset.pimage_congr {α : Type u_1} {β : Type u_2} [decidable_eq β] {f g : α →. β} [Π (x : α), decidable (f x).dom] [Π (x : α), decidable (g x).dom] {s t : finset α} (h₁ : s = t) (h₂ : (x : α), x t f x = g x) :
=
theorem finset.pimage_eq_image_filter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s : finset α} :
= finset.image (λ (x : {x // x finset.filter (λ (x : α), (f x).dom) s}), (f x).get _) (finset.filter (λ (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} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s t : finset α} [decidable_eq α] :
(s t) =
@[simp]
theorem finset.pimage_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] :
theorem finset.pimage_subset {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s : finset α} {t : finset β} :
t (x : α), x s (y : β), y f x y t
theorem finset.pimage_mono {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s t : finset α} (h : s t) :
theorem finset.pimage_inter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s t : finset α} [decidable_eq α] :
(s t)