mathlib3 documentation

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 #

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 α) :
@[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 finset.map f s (a : α) (H : a s), f a = b
@[simp]
theorem finset.mem_map_equiv {α : Type u_1} {β : Type u_2} {s : finset α} {f : α β} {b : β} :
theorem finset.mem_map' {α : Type u_1} {β : Type u_2} (f : α β) {a : α} {s : finset α} :
f a finset.map f s a s
theorem finset.mem_map_of_mem {α : Type u_1} {β : Type u_2} (f : α β) {a : α} {s : finset α} :
a s f a finset.map f s
theorem finset.forall_mem_map {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} {p : Π (a : β), a finset.map f s Prop} :
( (y : β) (H : y finset.map f 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) :
@[simp, norm_cast]
theorem finset.coe_map {α : Type u_1} {β : Type u_2} (f : α β) (s : finset α) :
theorem finset.coe_map_subset_range {α : Type u_1} {β : Type u_2} (f : α β) (s : finset α) :
theorem finset.map_perm {α : Type u_1} {s : finset α} {σ : equiv.perm α} (hs : {a : α | σ a a} 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 α) :
theorem finset.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : β γ) (s : finset α) :
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)) :
theorem function.semiconj.finset_map {α : Type u_1} {β : Type u_2} {f : α β} {ga : α α} {gb : β β} (h : function.semiconj f ga gb) :
@[simp]
theorem finset.map_subset_map {α : Type u_1} {β : Type u_2} {f : α β} {s₁ s₂ : finset α} :
finset.map f s₁ finset.map f 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 α} :
finset.map f s₁ = finset.map f 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 α} :
theorem finset.filter_map {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} {p : β Prop} [decidable_pred p] :
theorem finset.map_filter' {α : Type u_1} {β : Type u_2} (p : α Prop) [decidable_pred p] (f : α β) (s : finset α) [decidable_pred (λ (b : β), (a : α), p a f a = b)] :
finset.map f (finset.filter p s) = finset.filter (λ (b : β), (a : α), p a f a = b) (finset.map f s)
theorem finset.filter_attach' {α : Type u_1} [decidable_eq α] (s : finset α) (p : s Prop) [decidable_pred p] :
finset.filter p s.attach = finset.map {to_fun := subtype.map id _, inj' := _} (finset.filter (λ (x : α), (h : x s), p x, h⟩) s).attach
@[simp]
theorem finset.filter_attach {α : Type u_1} (p : α Prop) [decidable_pred p] (s : finset α) :
theorem finset.map_filter {α : Type u_1} {β : Type u_2} {s : finset α} {f : α β} {p : α Prop} [decidable_pred p] :
@[simp]
theorem finset.disjoint_map {α : Type u_1} {β : Type u_2} {s t : finset α} (f : α β) :
theorem finset.map_disj_union {α : Type u_1} {β : Type u_2} {f : α β} (s₁ s₂ : finset α) (h : disjoint s₁ s₂) (h' : disjoint (finset.map f s₁) (finset.map f s₂) := _) :
finset.map f (s₁.disj_union s₂ h) = (finset.map f s₁).disj_union (finset.map f s₂) h'
theorem finset.map_disj_union' {α : Type u_1} {β : Type u_2} {f : α β} (s₁ s₂ : finset α) (h' : disjoint (finset.map f s₁) (finset.map f s₂)) (h : disjoint s₁ s₂ := _) :
finset.map f (s₁.disj_union s₂ h) = (finset.map f s₁).disj_union (finset.map f 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 α) :
finset.map f (s₁ s₂) = finset.map f s₁ finset.map f s₂
theorem finset.map_inter {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α β} (s₁ s₂ : finset α) :
finset.map f (s₁ s₂) = finset.map f s₁ finset.map f s₂
@[simp]
theorem finset.map_singleton {α : Type u_1} {β : Type u_2} (f : α β) (a : α) :
finset.map f {a} = {f a}
@[simp]
theorem finset.map_insert {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α β) (a : α) (s : finset α) :
@[simp]
theorem finset.map_cons {α : Type u_1} {β : Type u_2} (f : α β) (a : α) (s : finset α) (ha : a s) :
@[simp]
theorem finset.map_eq_empty {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} :
@[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 : β finset γ} {h : (finset.map f s).pairwise_disjoint t} :
(finset.map f 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 : α finset β} {f : β γ} {h : s.pairwise_disjoint t} :
finset.map f (s.disj_Union t h) = s.disj_Union (λ (a : α), finset.map f (t a)) _
theorem finset.range_add_one' (n : ) :
finset.range (n + 1) = has_insert.insert 0 (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 α) :
@[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 finset.image f 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) :
theorem finset.forall_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} {p : β Prop} :
( (b : β), b finset.image f 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 : β} :
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)) [can_lift β α 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 : set.eq_on f g 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 finset.image f 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 finset.image f s) t = finset.image f 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 finset.image f s
@[simp, norm_cast]
theorem finset.coe_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {f : α β} :
@[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 : set.inj_on f s) :
@[simp]
theorem finset.image_id {α : Type u_1} {s : finset α} [decidable_eq α] :
@[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 : β γ} :
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)) :
theorem function.semiconj.finset_image {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} {ga : α α} {gb : β β} (h : function.semiconj f ga gb) :
theorem finset.image_subset_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s₁ s₂ : finset α} (h : s₁ s₂) :
theorem finset.image_subset_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} {t : finset β} :
finset.image f 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) :
theorem finset.coe_image_subset_range {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} :
theorem finset.image_filter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} {p : β Prop} [decidable_pred p] :
theorem finset.image_union {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} (s₁ s₂ : finset α) :
finset.image f (s₁ s₂) = finset.image f s₁ finset.image f s₂
theorem finset.image_inter_subset {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α β) (s t : finset α) :
theorem finset.image_inter_of_inj_on {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} (s t : finset α) (hf : set.inj_on f (s t)) :
theorem finset.image_inter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} [decidable_eq α] (s₁ s₂ : finset α) (hf : function.injective f) :
finset.image f (s₁ s₂) = finset.image f s₁ finset.image f s₂
@[simp]
theorem finset.image_singleton {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α β) (a : α) :
finset.image f {a} = {f a}
@[simp]
theorem finset.image_insert {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α β) (a : α) (s : finset α) :
theorem finset.erase_image_subset_image_erase {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α β) (s : finset α) (a : α) :
@[simp]
theorem finset.image_erase {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} (hf : function.injective f) (s : finset α) (a : α) :
finset.image f (s.erase a) = (finset.image f s).erase (f a)
@[simp]
theorem finset.image_eq_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α β} {s : finset α} :
theorem finset.image_sdiff {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} (s t : finset α) (hf : function.injective f) :
theorem finset.image_symm_diff {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α β} (s t : finset α) (hf : function.injective f) :
@[simp]
theorem disjoint.of_image_finset {α : Type u_1} {β : Type u_2} [decidable_eq β] {s t : finset α} {f : α β} (h : disjoint (finset.image f s) (finset.image f 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 set.range f 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 set.range f a finset.image (λ (i : ), f i) (finset.range n)
@[simp]
@[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 α} :
(has_insert.insert a 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 α) :
@[simp]
theorem finset.disjoint_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s t : finset α} {f : α β} (hf : function.injective f) :
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 : α) :
finset.map f (s.erase a) = (finset.map f 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 : β finset γ} :
(finset.image f 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 : α finset β} {f : β γ} :
finset.image f (s.bUnion t) = s.bUnion (λ (a : α), finset.image f (t a))
theorem finset.image_bUnion_filter_eq {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (s : finset β) (g : β α) :
(finset.image 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}) = finset.image f s

Subtype #

@[protected]
def finset.subtype {α : Type u_1} (p : α Prop) [decidable_pred p] (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} [decidable_pred p] {s : finset α} {a : subtype p} :
theorem finset.subtype_eq_empty {α : Type u_1} {p : α Prop} [decidable_pred p] {s : finset α} :
finset.subtype p s = (x : α), p x x s
theorem finset.subtype_mono {α : Type u_1} {p : α Prop} [decidable_pred p] :
@[simp]
theorem finset.subtype_map {α : Type u_1} (p : α Prop) [decidable_pred p] {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} [decidable_pred p] {s : finset α} (h : (x : α), x s p x) :

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) :
@[simp]
theorem finset.fin_map {n : } {s : finset } :
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 finset.image f s' = t
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]
@[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' : β γ) :