# mathlib3documentation

data.finset.image

# Image and map operations on finite sets #

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

Thie file provides the finite analog of set.image, along with some other similar functions.

Note there are two ways to take the image over a finset; via finset.image which applies the function then removes duplicates (requiring decidable_eq), or via finset.map which exploits injectivity of the function to avoid needing to deduplicate. Choosing between these is similar to choosing between insert and finset.cons, or between finset.union and finset.disj_union.

## Main definitions #

• finset.image: Given a function f : α → β, s.image f is the image finset in β.
• finset.map: Given an embedding f : α ↪ β, s.map f is the image finset in β.
• finset.subtype: s.subtype p is the the finset of subtype p whose elements belong to s.
• finset.fin:s.fin n is the finset of all elements of s less than n.

### map #

def finset.map {α : Type u_1} {β : Type u_2} (f : α β) (s : finset α) :

When f is an embedding of α in β and s is a finset in α, then s.map f is the image finset in β. The embedding condition guarantees that there are no duplicates in the image.

Equations
@[simp]
theorem finset.map_val {α : Type u_1} {β : Type u_2} (f : α β) (s : finset α) :
s).val = s.val
@[simp]
theorem finset.map_empty {α : Type u_1} {β : Type u_2} (f : α β) :
@[simp]
theorem finset.mem_map {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} {b : β} :
b s (a : α) (H : a s), f a = b
@[simp]
theorem finset.mem_map_equiv {α : Type u_1} {β : Type u_2} {s : finset α} {f : α β} {b : β} :
b (f.symm) b s
theorem finset.mem_map' {α : Type u_1} {β : Type u_2} (f : α β) {a : α} {s : finset α} :
f a s a s
theorem finset.mem_map_of_mem {α : Type u_1} {β : Type u_2} (f : α β) {a : α} {s : finset α} :
a s f a s
theorem finset.forall_mem_map {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} {p : Π (a : β), a s Prop} :
( (y : β) (H : y s), p y H) (x : α) (H : x s), p (f x) _
theorem finset.apply_coe_mem_map {α : Type u_1} {β : Type u_2} (f : α β) (s : finset α) (x : s) :
f x s
@[simp, norm_cast]
theorem finset.coe_map {α : Type u_1} {β : Type u_2} (f : α β) (s : finset α) :
s) = f '' s
theorem finset.coe_map_subset_range {α : Type u_1} {β : Type u_2} (f : α β) (s : finset α) :
s)
theorem finset.map_perm {α : Type u_1} {s : finset α} {σ : equiv.perm α} (hs : {a : α | σ a a} s) :
s = s

If the only elements outside s are those left fixed by σ, then mapping by σ has no effect.

theorem finset.map_to_finset {α : Type u_1} {β : Type u_2} {f : α β} [decidable_eq α] [decidable_eq β] {s : multiset α} :
@[simp]
theorem finset.map_refl {α : Type u_1} {s : finset α} :
@[simp]
theorem finset.map_cast_heq {α β : Type u_1} (h : α = β) (s : finset α) :
== s
theorem finset.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : β γ) (s : finset α) :
s) = finset.map (f.trans g) s
theorem finset.map_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : finset α} {β' : Type u_4} {f : β γ} {g : α β} {f' : α β'} {g' : β' γ} (h_comm : (a : α), f (g a) = g' (f' a)) :
s) = (finset.map f' s)
theorem function.semiconj.finset_map {α : Type u_1} {β : Type u_2} {f : α β} {ga : α α} {gb : β β} (h : gb) :
theorem function.commute.finset_map {α : Type u_1} {f g : α α} (h : g) :
@[simp]
theorem finset.map_subset_map {α : Type u_1} {β : Type u_2} {f : α β} {s₁ s₂ : finset α} :
s₁ s₂ s₁ s₂
def finset.map_embedding {α : Type u_1} {β : Type u_2} (f : α β) :

Associate to an embedding f from α to β the order embedding that maps a finset to its image under f.

Equations
@[simp]
theorem finset.map_inj {α : Type u_1} {β : Type u_2} {f : α β} {s₁ s₂ : finset α} :
s₁ = s₂ s₁ = s₂
theorem finset.map_injective {α : Type u_1} {β : Type u_2} (f : α β) :
@[simp]
theorem finset.map_embedding_apply {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} :
= s
theorem finset.filter_map {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} {p : β Prop}  :
s) = (finset.filter (p f) s)
theorem finset.map_filter' {α : Type u_1} {β : Type u_2} (p : α Prop) (f : α β) (s : finset α) [decidable_pred (λ (b : β), (a : α), p a f a = b)] :
s) = finset.filter (λ (b : β), (a : α), p a f a = b) s)
theorem finset.filter_attach' {α : Type u_1} [decidable_eq α] (s : finset α) (p : s Prop)  :
= finset.map {to_fun := , inj' := _} (finset.filter (λ (x : α), (h : x s), p x, h⟩) s).attach
@[simp]
theorem finset.filter_attach {α : Type u_1} (p : α Prop) (s : finset α) :
finset.filter (λ (x : {x // x s}), p x) s.attach =
theorem finset.map_filter {α : Type u_1} {β : Type u_2} {s : finset α} {f : α β} {p : α Prop}  :
s) = finset.filter (p (f.symm)) s)
@[simp]
theorem finset.disjoint_map {α : Type u_1} {β : Type u_2} {s t : finset α} (f : α β) :
disjoint s) t) t
theorem finset.map_disj_union {α : Type u_1} {β : Type u_2} {f : α β} (s₁ s₂ : finset α) (h : disjoint s₁ s₂) (h' : disjoint s₁) s₂) := _) :
(s₁.disj_union s₂ h) = s₁).disj_union s₂) h'
theorem finset.map_disj_union' {α : Type u_1} {β : Type u_2} {f : α β} (s₁ s₂ : finset α) (h' : disjoint s₁) s₂)) (h : disjoint s₁ s₂ := _) :
(s₁.disj_union s₂ h) = s₁).disj_union s₂) h'

A version of finset.map_disj_union for writing in the other direction.

theorem finset.map_union {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α β} (s₁ s₂ : finset α) :
(s₁ s₂) = s₁ s₂
theorem finset.map_inter {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α β} (s₁ s₂ : finset α) :
(s₁ s₂) = s₁ s₂
@[simp]
theorem finset.map_singleton {α : Type u_1} {β : Type u_2} (f : α β) (a : α) :
{a} = {f a}
@[simp]
theorem finset.map_insert {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α β) (a : α) (s : finset α) :
s) = has_insert.insert (f a) s)
@[simp]
theorem finset.map_cons {α : Type u_1} {β : Type u_2} (f : α β) (a : α) (s : finset α) (ha : a s) :
s ha) = finset.cons (f a) s) _
@[simp]
theorem finset.map_eq_empty {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} :
s = s =
@[simp]
theorem finset.map_nonempty {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} :
theorem finset.nonempty.map {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} :

Alias of the reverse direction of finset.map_nonempty.

theorem finset.attach_map_val {α : Type u_1} {s : finset α} :
theorem finset.map_disj_Union {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {s : finset α} {t : β } {h : s).pairwise_disjoint t} :
s).disj_Union t h = s.disj_Union (λ (a : α), t (f a)) _
theorem finset.disj_Union_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : finset α} {t : α } {f : β γ} {h : s.pairwise_disjoint t} :
(s.disj_Union t h) = s.disj_Union (λ (a : α), (t a)) _
theorem finset.range_add_one' (n : ) :
finset.range (n + 1) = (finset.map {to_fun := λ (i : ), i + 1, inj' := _} (finset.range n))

### image #

def finset.image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α β) (s : finset α) :

image f s is the forward image of s under f.

Equations
Instances for finset.image
@[simp]
theorem finset.image_val {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α β) (s : finset α) :
s).val = s.val).dedup
@[simp]
theorem finset.image_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α β) :
@[simp]
theorem finset.mem_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} {b : β} :
b s (a : α) (H : a s), f a = b
theorem finset.mem_image_of_mem {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (f : α β) {a : α} (h : a s) :
f a s
theorem finset.forall_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} {p : β Prop} :
( (b : β), b s p b) (a : α), a s p (f a)
@[simp]
theorem finset.mem_image_const {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {b c : β} :
c s s.nonempty b = c
theorem finset.mem_image_const_self {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {b : β} :
@[protected, instance]
def finset.can_lift {α : Type u_1} {β : Type u_2} [decidable_eq β] (c : out_param β)) (p : out_param Prop)) [ α c p] :
can_lift (finset β) (finset α) (finset.image c) (λ (s : finset β), (x : β), x s p x)
Equations
theorem finset.image_congr {α : Type u_1} {β : Type u_2} [decidable_eq β] {f g : α β} {s : finset α} (h : g s) :
s = s
theorem function.injective.mem_finset_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} {a : α} (hf : function.injective f) :
f a s a s
theorem finset.filter_mem_image_eq_image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α β) (s : finset α) (t : finset β) (h : (x : α), x s f x t) :
finset.filter (λ (y : β), y s) t = s
theorem finset.fiber_nonempty_iff_mem_image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α β) (s : finset α) (y : β) :
(finset.filter (λ (x : α), f x = y) s).nonempty y s
@[simp, norm_cast]
theorem finset.coe_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {f : α β} :
s) = f '' s
@[protected]
theorem finset.nonempty.image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (h : s.nonempty) (f : α β) :
@[simp]
theorem finset.nonempty.image_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (f : α β) :
theorem finset.image_to_finset {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} [decidable_eq α] {s : multiset α} :
theorem finset.image_val_of_inj_on {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} (H : s) :
s).val = s.val
@[simp]
theorem finset.image_id {α : Type u_1} {s : finset α} [decidable_eq α] :
= s
@[simp]
theorem finset.image_id' {α : Type u_1} {s : finset α} [decidable_eq α] :
finset.image (λ (x : α), x) s = s
theorem finset.image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] {f : α β} {s : finset α} [decidable_eq γ] {g : β γ} :
s) = finset.image (g f) s
theorem finset.image_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] {s : finset α} {β' : Type u_4} [decidable_eq β'] [decidable_eq γ] {f : β γ} {g : α β} {f' : α β'} {g' : β' γ} (h_comm : (a : α), f (g a) = g' (f' a)) :
s) = (finset.image f' s)
theorem function.semiconj.finset_image {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} {ga : α α} {gb : β β} (h : gb) :
theorem function.commute.finset_image {α : Type u_1} [decidable_eq α] {f g : α α} (h : g) :
theorem finset.image_subset_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s₁ s₂ : finset α} (h : s₁ s₂) :
s₁ s₂
theorem finset.image_subset_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} {t : finset β} :
s t (x : α), x s f x t
theorem finset.image_mono {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α β) :
theorem finset.image_subset_image_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s t : finset α} (hf : function.injective f) :
s t s t
theorem finset.coe_image_subset_range {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} :
s)
theorem finset.image_filter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} {p : β Prop}  :
s) = (finset.filter (p f) s)
theorem finset.image_union {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} (s₁ s₂ : finset α) :
(s₁ s₂) = s₁ s₂
theorem finset.image_inter_subset {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α β) (s t : finset α) :
(s t) s t
theorem finset.image_inter_of_inj_on {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} (s t : finset α) (hf : (s t)) :
(s t) = s t
theorem finset.image_inter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} [decidable_eq α] (s₁ s₂ : finset α) (hf : function.injective f) :
(s₁ s₂) = s₁ s₂
@[simp]
theorem finset.image_singleton {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α β) (a : α) :
{a} = {f a}
@[simp]
theorem finset.image_insert {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α β) (a : α) (s : finset α) :
s) = has_insert.insert (f a) s)
theorem finset.erase_image_subset_image_erase {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α β) (s : finset α) (a : α) :
s).erase (f a) (s.erase a)
@[simp]
theorem finset.image_erase {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} (hf : function.injective f) (s : finset α) (a : α) :
(s.erase a) = s).erase (f a)
@[simp]
theorem finset.image_eq_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} :
s = s =
theorem finset.image_sdiff {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} (s t : finset α) (hf : function.injective f) :
(s \ t) = s \ t
theorem finset.image_symm_diff {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} (s t : finset α) (hf : function.injective f) :
(s t) = s t
@[simp]
theorem disjoint.of_image_finset {α : Type u_1} {β : Type u_2} [decidable_eq β] {s t : finset α} {f : α β} (h : disjoint s) t)) :
t
theorem finset.mem_range_iff_mem_finset_range_of_mod_eq' {α : Type u_1} [decidable_eq α] {f : α} {a : α} {n : } (hn : 0 < n) (h : (i : ), f (i % n) = f i) :
a a finset.image (λ (i : ), f i) (finset.range n)
theorem finset.mem_range_iff_mem_finset_range_of_mod_eq {α : Type u_1} [decidable_eq α] {f : α} {a : α} {n : } (hn : 0 < n) (h : (i : ), f (i % n) = f i) :
a a finset.image (λ (i : ), f i) (finset.range n)
theorem finset.range_add (a b : ) :
@[simp]
theorem finset.attach_image_val {α : Type u_1} [decidable_eq α] {s : finset α} :
@[simp]
theorem finset.attach_image_coe {α : Type u_1} [decidable_eq α] {s : finset α} :
@[simp]
theorem finset.attach_insert {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
s).attach = has_insert.insert a, _⟩ (finset.image (λ (x : {x // x s}), x.val, _⟩) s.attach)
theorem finset.map_eq_image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α β) (s : finset α) :
s =
@[simp]
theorem finset.disjoint_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s t : finset α} {f : α β} (hf : function.injective f) :
disjoint s) t) t
theorem finset.image_const {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (h : s.nonempty) (b : β) :
finset.image (λ (a : α), b) s = {b}
@[simp]
theorem finset.map_erase {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α β) (s : finset α) (a : α) :
(s.erase a) = s).erase (f a)
theorem finset.image_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [decidable_eq γ] {f : α β} {s : finset α} {t : β } :
s).bUnion t = s.bUnion (λ (a : α), t (f a))
theorem finset.bUnion_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [decidable_eq γ] {s : finset α} {t : α } {f : β γ} :
(s.bUnion t) = s.bUnion (λ (a : α), (t a))
theorem finset.image_bUnion_filter_eq {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (s : finset β) (g : β α) :
s).bUnion (λ (a : α), finset.filter (λ (c : β), g c = a) s) = s
theorem finset.bUnion_singleton {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {f : α β} :
s.bUnion (λ (a : α), {f a}) = s

### Subtype #

@[protected]
def finset.subtype {α : Type u_1} (p : α Prop) (s : finset α) :

Given a finset s and a predicate p, s.subtype p is the finset of subtype p whose elements belong to s.

Equations
@[simp]
theorem finset.mem_subtype {α : Type u_1} {p : α Prop} {s : finset α} {a : subtype p} :
a a s
theorem finset.subtype_eq_empty {α : Type u_1} {p : α Prop} {s : finset α} :
= (x : α), p x x s
theorem finset.subtype_mono {α : Type u_1} {p : α Prop}  :
@[simp]
theorem finset.subtype_map {α : Type u_1} (p : α Prop) {s : finset α} :
=

s.subtype p converts back to s.filter p with embedding.subtype.

theorem finset.subtype_map_of_mem {α : Type u_1} {p : α Prop} {s : finset α} (h : (x : α), x s p x) :
= s

If all elements of a finset satisfy the predicate p, s.subtype p converts back to s with embedding.subtype.

theorem finset.property_of_mem_map_subtype {α : Type u_1} {p : α Prop} (s : finset {x // p x}) {a : α} (h : a finset.map (function.embedding.subtype (λ (x : α), p x)) s) :
p a

If a finset of a subtype is converted to the main type with embedding.subtype, all elements of the result have the property of the subtype.

theorem finset.not_mem_map_subtype_of_not_property {α : Type u_1} {p : α Prop} (s : finset {x // p x}) {a : α} (h : ¬p a) :
a finset.map (function.embedding.subtype (λ (x : α), p x)) s

If a finset of a subtype is converted to the main type with embedding.subtype, the result does not contain any value that does not satisfy the property of the subtype.

theorem finset.map_subtype_subset {α : Type u_1} {t : set α} (s : finset t) :
(finset.map (function.embedding.subtype (λ (x : α), x t)) s) t

If a finset of a subtype is converted to the main type with embedding.subtype, the result is a subset of the set giving the subtype.

### Fin #

@[protected]
def finset.fin (n : ) (s : finset ) :

Given a finset s of natural numbers and a bound n, s.fin n is the finset of all elements of s less than n.

Equations
@[simp]
theorem finset.mem_fin {n : } {s : finset } (a : fin n) :
a s a s
theorem finset.fin_mono {n : } :
@[simp]
theorem finset.fin_map {n : } {s : finset } :
= finset.filter (λ (_x : ), _x < n) s
theorem finset.subset_image_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : set α} {t : finset β} {f : α β} :
t f '' s (s' : finset α), s' s s' = t
theorem finset.range_sdiff_zero {n : } :
finset.range (n + 1) \ {0} =
theorem multiset.to_finset_map {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α β) (m : multiset α) :
@[protected]
def equiv.finset_congr {α : Type u_1} {β : Type u_2} (e : α β) :

Given an equivalence α to β, produce an equivalence between finset α and finset β.

Equations
@[simp]
theorem equiv.finset_congr_apply {α : Type u_1} {β : Type u_2} (e : α β) (s : finset α) :
@[simp]
theorem equiv.finset_congr_refl {α : Type u_1} :
@[simp]
theorem equiv.finset_congr_symm {α : Type u_1} {β : Type u_2} (e : α β) :
@[simp]
theorem equiv.finset_congr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (e' : β γ) :
theorem equiv.finset_congr_to_embedding {α : Type u_1} {β : Type u_2} (e : α β) :