Image and map operations on finite sets

This 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 DecidableEq), 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.disjUnion.

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.filterMap Given a function f : α → Option β, s.filterMap f is the image finset in β, filtering out nones.
• Finset.subtype: s.subtype p is 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.

TODO

Move the material about Finset.range so that the Mathlib.Algebra.Group.Embedding import can be removed.

map

def Finset.map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : 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

• Finset.map f s = { val := Multiset.map (⇑f) s.val, nodup := ⋯ }

@[simp]

theorem Finset.map_val {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : (Finset.map f s).val = Multiset.map (⇑f) s.val

@[simp]

theorem Finset.map_empty {α : Type u_1} {β : Type u_2} (f : α ↪ β) : Finset.map f ∅ = ∅

@[simp]

theorem Finset.mem_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {b : β} : b ∈ Finset.map f s ↔ ∃ a ∈ s, f a = b

@[simp]

theorem Finset.mem_map_equiv {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {b : β} : b ∈ Finset.map f.toEmbedding s ↔ f.symm b ∈ s

@[simp]

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 : { x : α // x ∈ s }) : f ↑x ∈ Finset.map f s

@[simp]

theorem Finset.coe_map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : ↑(Finset.map f s) = ⇑f '' ↑s

theorem Finset.coe_map_subset_range {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : ↑(Finset.map f s) ⊆ Set.range ⇑f

theorem Finset.map_perm {α : Type u_1} {s : Finset α} {σ : Equiv.Perm α} (hs : {a : α | σ a ≠ a} ⊆ ↑s) : Finset.map (Equiv.toEmbedding σ) s = s

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

theorem Finset.map_toFinset {α : Type u_1} {β : Type u_2} {f : α ↪ β} [DecidableEq α] [DecidableEq β] {s : Multiset α} : Finset.map f s.toFinset = (Multiset.map (⇑f) s).toFinset

@[simp]

theorem Finset.map_refl {α : Type u_1} {s : Finset α} : Finset.map (Function.Embedding.refl α) s = s

@[simp]

theorem Finset.map_cast_heq {α : Type u_4} {β : Type u_4} (h : α = β) (s : Finset α) : HEq (Finset.map (Equiv.cast h).toEmbedding s) s

theorem Finset.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ↪ β) (g : β ↪ γ) (s : Finset α) : Finset.map g (Finset.map f 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)) : Finset.map f (Finset.map g s) = Finset.map g' (Finset.map f' s)

theorem Function.Semiconj.finset_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {ga : α ↪ α} {gb : β ↪ β} (h : Function.Semiconj ⇑f ⇑ga ⇑gb) : Function.Semiconj (Finset.map f) (Finset.map ga) (Finset.map gb)

theorem Function.Commute.finset_map {α : Type u_1} {f : α ↪ α} {g : α ↪ α} (h : Function.Commute ⇑f ⇑g) : Function.Commute (Finset.map f) (Finset.map g)

@[simp]

theorem Finset.map_subset_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ : Finset α} {s₂ : Finset α} : Finset.map f s₁ ⊆ Finset.map f s₂ ↔ s₁ ⊆ s₂

theorem GCongr.finsetMap_subset {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ : Finset α} {s₂ : Finset α} : s₁ ⊆ s₂ → Finset.map f s₁ ⊆ Finset.map f s₂

Alias of the reverse direction of Finset.map_subset_map.

theorem Finset.subset_map_symm {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : α ≃ β} : s ⊆ Finset.map f.symm.toEmbedding t ↔ Finset.map f.toEmbedding s ⊆ t

The Finset version of Equiv.subset_symm_image.

theorem Finset.map_symm_subset {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : α ≃ β} : Finset.map f.symm.toEmbedding t ⊆ s ↔ t ⊆ Finset.map f.toEmbedding s

The Finset version of Equiv.symm_image_subset.

def Finset.mapEmbedding {α : Type u_1} {β : Type u_2} (f : α ↪ β) : Finset α ↪o Finset β

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

Equations

• Finset.mapEmbedding f = OrderEmbedding.ofMapLEIff (Finset.map f) ⋯

@[simp]

theorem Finset.map_inj {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ : Finset α} {s₂ : Finset α} : Finset.map f s₁ = Finset.map f s₂ ↔ s₁ = s₂

theorem Finset.map_injective {α : Type u_1} {β : Type u_2} (f : α ↪ β) : Function.Injective (Finset.map f)

@[simp]

theorem Finset.map_ssubset_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {t : Finset α} : Finset.map f s ⊂ Finset.map f t ↔ s ⊂ t

theorem GCongr.finsetMap_ssubset {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {t : Finset α} : s ⊂ t → Finset.map f s ⊂ Finset.map f t

Alias of the reverse direction of Finset.map_ssubset_map.

@[simp]

theorem Finset.mapEmbedding_apply {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} : (Finset.mapEmbedding f) s = Finset.map f s

theorem Finset.filter_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {p : β → Prop} [DecidablePred p] : Finset.filter p (Finset.map f s) = Finset.map f (Finset.filter (p ∘ ⇑f) s)

theorem Finset.map_filter' {α : Type u_1} {β : Type u_2} (p : α → Prop) [DecidablePred p] (f : α ↪ β) (s : Finset α) [DecidablePred fun (x : β) => ∃ (a : α), p a ∧ f a = x] : Finset.map f (Finset.filter p s) = Finset.filter (fun (b : β) => ∃ (a : α), p a ∧ f a = b) (Finset.map f s)

theorem Finset.filter_attach' {α : Type u_1} [DecidableEq α] (s : Finset α) (p : { x : α // x ∈ s } → Prop) [DecidablePred p] : Finset.filter p s.attach = Finset.map { toFun := Subtype.map id ⋯, inj' := ⋯ } (Finset.filter (fun (x : α) => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach

theorem Finset.filter_attach {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset.filter (fun (a : { x : α // x ∈ s }) => p ↑a) s.attach = Finset.map ((Function.Embedding.refl α).subtypeMap ⋯) (Finset.filter p s).attach

theorem Finset.map_filter {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {p : α → Prop} [DecidablePred p] : Finset.map f.toEmbedding (Finset.filter p s) = Finset.filter (p ∘ ⇑f.symm) (Finset.map f.toEmbedding s)

@[simp]

theorem Finset.disjoint_map {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset α} (f : α ↪ β) : Disjoint (Finset.map f s) (Finset.map f t) ↔ Disjoint s t

theorem Finset.map_disjUnion {α : Type u_1} {β : Type u_2} {f : α ↪ β} (s₁ : Finset α) (s₂ : Finset α) (h : Disjoint s₁ s₂) (h' : optParam (Disjoint (Finset.map f s₁) (Finset.map f s₂)) ⋯) : Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'

theorem Finset.map_disjUnion' {α : Type u_1} {β : Type u_2} {f : α ↪ β} (s₁ : Finset α) (s₂ : Finset α) (h' : Disjoint (Finset.map f s₁) (Finset.map f s₂)) (h : optParam (Disjoint s₁ s₂) ⋯) : Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'

A version of Finset.map_disjUnion for writing in the other direction.

theorem Finset.map_union {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ : Finset α) (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} [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ : Finset α) (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} [DecidableEq α] [DecidableEq β] (f : α ↪ β) (a : α) (s : Finset α) : Finset.map f (insert a s) = insert (f a) (Finset.map f s)

@[simp]

theorem Finset.map_cons {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : α) (s : Finset α) (ha : a ∉ s) : Finset.map f (Finset.cons a s ha) = Finset.cons (f a) (Finset.map f s) ⋯

@[simp]

theorem Finset.map_eq_empty {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} : Finset.map f s = ∅ ↔ s = ∅

@[simp]

theorem Finset.map_nonempty {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} : (Finset.map f s).Nonempty ↔ s.Nonempty

theorem Finset.Nonempty.map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} : s.Nonempty → (Finset.map f s).Nonempty

Alias of the reverse direction of Finset.map_nonempty.

@[simp]

theorem Finset.map_nontrivial {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} : (Finset.map f s).Nontrivial ↔ s.Nontrivial

theorem Finset.attach_map_val {α : Type u_1} {s : Finset α} : Finset.map (Function.Embedding.subtype fun (x : α) => x ∈ s) s.attach = s

theorem Finset.disjoint_range_addLeftEmbedding (a : ℕ) (s : Finset ℕ) : Disjoint (Finset.range a) (Finset.map (addLeftEmbedding a) s)

theorem Finset.disjoint_range_addRightEmbedding (a : ℕ) (s : Finset ℕ) : Disjoint (Finset.range a) (Finset.map (addRightEmbedding a) s)

theorem Finset.map_disjiUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α ↪ β} {s : Finset α} {t : β → Finset γ} {h : (↑(Finset.map f s)).PairwiseDisjoint t} : (Finset.map f s).disjiUnion t h = s.disjiUnion (fun (a : α) => t (f a)) ⋯

theorem Finset.disjiUnion_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : α → Finset β} {f : β ↪ γ} {h : (↑s).PairwiseDisjoint t} : Finset.map f (s.disjiUnion t h) = s.disjiUnion (fun (a : α) => Finset.map f (t a)) ⋯

theorem Finset.range_add_one' (n : ℕ) : Finset.range (n + 1) = insert 0 (Finset.map { toFun := fun (i : ℕ) => i + 1, inj' := ⋯ } (Finset.range n))

image

def Finset.image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Finset α) : Finset β

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

Equations

• Finset.image f s = (Multiset.map f s.val).toFinset

@[simp]

theorem Finset.image_val {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Finset α) : (Finset.image f s).val = (Multiset.map f s.val).dedup

@[simp]

theorem Finset.image_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) : Finset.image f ∅ = ∅

@[simp]

theorem Finset.mem_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {b : β} : b ∈ Finset.image f s ↔ ∃ a ∈ s, f a = b

theorem Finset.mem_image_of_mem {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (f : α → β) {a : α} (h : a ∈ s) : f a ∈ Finset.image f s

theorem Finset.forall_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop} : (∀ b ∈ Finset.image f s, p b) ↔ ∀ a ∈ s, p (f a)

theorem Finset.map_eq_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α ↪ β) (s : Finset α) : Finset.map f s = Finset.image (⇑f) s

theorem Finset.mem_image_const {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {b : β} {c : β} : c ∈ Finset.image (Function.const α b) s ↔ s.Nonempty ∧ b = c

theorem Finset.mem_image_const_self {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {b : β} : b ∈ Finset.image (Function.const α b) s ↔ s.Nonempty

instance Finset.canLift {α : Type u_1} {β : Type u_2} [DecidableEq β] (c : α → β) (p : β → Prop) [CanLift β α c p] : CanLift (Finset β) (Finset α) (Finset.image c) fun (s : Finset β) => ∀ x ∈ s, p x

Equations

• ⋯ = ⋯

theorem Finset.image_congr {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {g : α → β} {s : Finset α} (h : Set.EqOn f g ↑s) : Finset.image f s = Finset.image g s

theorem Function.Injective.mem_finset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {a : α} (hf : Function.Injective f) : f a ∈ Finset.image f s ↔ a ∈ s

@[simp]

theorem Finset.coe_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} : ↑(Finset.image f s) = f '' ↑s

@[simp]

theorem Finset.image_nonempty {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} : (Finset.image f s).Nonempty ↔ s.Nonempty

theorem Finset.Nonempty.image {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (h : s.Nonempty) (f : α → β) : (Finset.image f s).Nonempty

theorem Finset.Nonempty.of_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} : (Finset.image f s).Nonempty → s.Nonempty

Alias of the forward direction of Finset.image_nonempty.

@[deprecated Finset.image_nonempty]

theorem Finset.Nonempty.image_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (f : α → β) : (Finset.image f s).Nonempty ↔ s.Nonempty

theorem Finset.image_toFinset {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} [DecidableEq α] {s : Multiset α} : Finset.image f s.toFinset = (Multiset.map f s).toFinset

theorem Finset.image_val_of_injOn {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} (H : Set.InjOn f ↑s) : (Finset.image f s).val = Multiset.map f s.val

@[simp]

theorem Finset.image_id {α : Type u_1} {s : Finset α} [DecidableEq α] : Finset.image id s = s

@[simp]

theorem Finset.image_id' {α : Type u_1} {s : Finset α} [DecidableEq α] : Finset.image (fun (x : α) => x) s = s

theorem Finset.image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] {f : α → β} {s : Finset α} [DecidableEq γ] {g : β → γ} : Finset.image g (Finset.image f s) = Finset.image (g ∘ f) s

theorem Finset.image_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] {s : Finset α} {β' : Type u_4} [DecidableEq β'] [DecidableEq γ] {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ} (h_comm : ∀ (a : α), f (g a) = g' (f' a)) : Finset.image f (Finset.image g s) = Finset.image g' (Finset.image f' s)

theorem Function.Semiconj.finset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : α → β} {ga : α → α} {gb : β → β} (h : Function.Semiconj f ga gb) : Function.Semiconj (Finset.image f) (Finset.image ga) (Finset.image gb)

theorem Function.Commute.finset_image {α : Type u_1} [DecidableEq α] {f : α → α} {g : α → α} (h : Function.Commute f g) : Function.Commute (Finset.image f) (Finset.image g)

theorem Finset.image_subset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s₁ : Finset α} {s₂ : Finset α} (h : s₁ ⊆ s₂) : Finset.image f s₁ ⊆ Finset.image f s₂

theorem Finset.image_subset_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} : Finset.image f s ⊆ t ↔ ∀ x ∈ s, f x ∈ t

theorem Finset.image_mono {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) : Monotone (Finset.image f)

theorem Finset.image_injective {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} (hf : Function.Injective f) : Function.Injective (Finset.image f)

theorem Finset.image_inj {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset α} (hf : Function.Injective f) : Finset.image f s = Finset.image f t ↔ s = t

theorem Finset.image_subset_image_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset α} (hf : Function.Injective f) : Finset.image f s ⊆ Finset.image f t ↔ s ⊆ t

theorem Finset.image_ssubset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset α} (hf : Function.Injective f) : Finset.image f s ⊂ Finset.image f t ↔ s ⊂ t

theorem Finset.coe_image_subset_range {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} : ↑(Finset.image f s) ⊆ Set.range f

theorem Finset.filter_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop} [DecidablePred p] : Finset.filter p (Finset.image f s) = Finset.image f (Finset.filter (fun (a : α) => p (f a)) s)

@[deprecated Finset.filter_mem_eq_inter]

theorem Finset.filter_mem_image_eq_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Finset α) (t : Finset β) (h : ∀ x ∈ s, f x ∈ t) : Finset.filter (fun (y : β) => y ∈ Finset.image f s) t = Finset.image f s

theorem Finset.fiber_nonempty_iff_mem_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {y : β} : (Finset.filter (fun (x : α) => f x = y) s).Nonempty ↔ y ∈ Finset.image f s

theorem Finset.image_union {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : α → β} (s₁ : Finset α) (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} [DecidableEq β] [DecidableEq α] (f : α → β) (s : Finset α) (t : Finset α) : Finset.image f (s ∩ t) ⊆ Finset.image f s ∩ Finset.image f t

theorem Finset.image_inter_of_injOn {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : α → β} (s : Finset α) (t : Finset α) (hf : Set.InjOn f (↑s ∪ ↑t)) : Finset.image f (s ∩ t) = Finset.image f s ∩ Finset.image f t

theorem Finset.image_inter {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} [DecidableEq α] (s₁ : Finset α) (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} [DecidableEq β] (f : α → β) (a : α) : Finset.image f {a} = {f a}

@[simp]

theorem Finset.image_insert {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : α → β) (a : α) (s : Finset α) : Finset.image f (insert a s) = insert (f a) (Finset.image f s)

theorem Finset.erase_image_subset_image_erase {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : α → β) (s : Finset α) (a : α) : (Finset.image f s).erase (f a) ⊆ Finset.image f (s.erase a)

@[simp]

theorem Finset.image_erase {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {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} [DecidableEq β] {f : α → β} {s : Finset α} : Finset.image f s = ∅ ↔ s = ∅

theorem Finset.image_sdiff {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : α → β} (s : Finset α) (t : Finset α) (hf : Function.Injective f) : Finset.image f (s \ t) = Finset.image f s \ Finset.image f t

theorem Finset.image_symmDiff {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : α → β} (s : Finset α) (t : Finset α) (hf : Function.Injective f) : Finset.image f (symmDiff s t) = symmDiff (Finset.image f s) (Finset.image f t)

@[simp]

theorem Disjoint.of_image_finset {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : Finset α} {f : α → β} (h : Disjoint (Finset.image f s) (Finset.image f t)) : Disjoint s t

theorem Finset.mem_range_iff_mem_finset_range_of_mod_eq' {α : Type u_1} [DecidableEq α] {f : ℕ → α} {a : α} {n : ℕ} (hn : 0 < n) (h : ∀ (i : ℕ), f (i % n) = f i) : a ∈ Set.range f ↔ a ∈ Finset.image (fun (i : ℕ) => f i) (Finset.range n)

theorem Finset.mem_range_iff_mem_finset_range_of_mod_eq {α : Type u_1} [DecidableEq α] {f : ℤ → α} {a : α} {n : ℕ} (hn : 0 < n) (h : ∀ (i : ℤ), f (i % ↑n) = f i) : a ∈ Set.range f ↔ a ∈ Finset.image (fun (i : ℕ) => f ↑i) (Finset.range n)

theorem Finset.range_add (a : ℕ) (b : ℕ) : Finset.range (a + b) = Finset.range a ∪ Finset.map (addLeftEmbedding a) (Finset.range b)

@[simp]

theorem Finset.attach_image_val {α : Type u_1} [DecidableEq α] {s : Finset α} : Finset.image Subtype.val s.attach = s

@[simp]

theorem Finset.attach_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} : (insert a s).attach = insert ⟨a, ⋯⟩ (Finset.image (fun (x : { x : α // x ∈ s }) => ⟨↑x, ⋯⟩) s.attach)

@[simp]

theorem Finset.disjoint_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : Finset α} {f : α → β} (hf : Function.Injective f) : Disjoint (Finset.image f s) (Finset.image f t) ↔ Disjoint s t

theorem Finset.image_const {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (h : s.Nonempty) (b : β) : Finset.image (fun (x : α) => b) s = {b}

@[simp]

theorem Finset.map_erase {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : α ↪ β) (s : Finset α) (a : α) : Finset.map f (s.erase a) = (Finset.map f s).erase (f a)

theorem Finset.image_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {f : α → β} {s : Finset α} {t : β → Finset γ} : (Finset.image f s).biUnion t = s.biUnion fun (a : α) => t (f a)

theorem Finset.biUnion_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {s : Finset α} {t : α → Finset β} {f : β → γ} : Finset.image f (s.biUnion t) = s.biUnion fun (a : α) => Finset.image f (t a)

theorem Finset.image_biUnion_filter_eq {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (s : Finset β) (g : β → α) : ((Finset.image g s).biUnion fun (a : α) => Finset.filter (fun (c : β) => g c = a) s) = s

theorem Finset.biUnion_singleton {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {f : α → β} : (s.biUnion fun (a : α) => {f a}) = Finset.image f s

filterMap

def Finset.filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (s : Finset α) (f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a') : Finset β

filterMap f s is a combination filter/map operation on s. The function f : α → Option β is applied to each element of s; if f a is some b then b is included in the result, otherwise a is excluded from the resulting finset.

In notation, filterMap f s is the finset {b : β | ∃ a ∈ s , f a = some b}.

Equations

• Finset.filterMap f s f_inj = { val := Multiset.filterMap f s.val, nodup := ⋯ }

@[simp]

theorem Finset.filterMap_val {α : Type u_1} {β : Type u_2} (f : α → Option β) (s' : Finset α) {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'} : (Finset.filterMap f s' f_inj).val = Multiset.filterMap f s'.val

@[simp]

theorem Finset.filterMap_empty {α : Type u_1} {β : Type u_2} (f : α → Option β) {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'} : Finset.filterMap f ∅ f_inj = ∅

@[simp]

theorem Finset.mem_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) {s : Finset α} {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'} {b : β} : b ∈ Finset.filterMap f s f_inj ↔ ∃ a ∈ s, f a = some b

@[simp]

theorem Finset.coe_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) {s : Finset α} {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'} : ↑(Finset.filterMap f s f_inj) = {b : β | ∃ a ∈ s, f a = some b}

@[simp]

theorem Finset.filterMap_some {α : Type u_1} {s : Finset α} : Finset.filterMap some s ⋯ = s

theorem Finset.filterMap_mono {α : Type u_1} {β : Type u_2} (f : α → Option β) {s : Finset α} {t : Finset α} {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'} (h : s ⊆ t) : Finset.filterMap f s f_inj ⊆ Finset.filterMap f t f_inj

Subtype

def Finset.subtype {α : Type u_4} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset (Subtype p)

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

Equations

• Finset.subtype p s = Finset.map { toFun := fun (x : { x : α // x ∈ Finset.filter p s }) => ⟨↑x, ⋯⟩, inj' := ⋯ } (Finset.filter p s).attach

@[simp]

theorem Finset.mem_subtype {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} {a : Subtype p} : a ∈ Finset.subtype p s ↔ ↑a ∈ s

theorem Finset.subtype_eq_empty {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} : Finset.subtype p s = ∅ ↔ ∀ (x : α), p x → x ∉ s

theorem Finset.subtype_mono {α : Type u_1} {p : α → Prop} [DecidablePred p] : Monotone (Finset.subtype p)

@[simp]

theorem Finset.subtype_map {α : Type u_1} (p : α → Prop) [DecidablePred p] {s : Finset α} : Finset.map (Function.Embedding.subtype p) (Finset.subtype p s) = Finset.filter p s

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

theorem Finset.subtype_map_of_mem {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} (h : ∀ x ∈ s, p x) : Finset.map (Function.Embedding.subtype p) (Finset.subtype p s) = 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 fun (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 fun (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 fun (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

def Finset.fin (n : ℕ) (s : Finset ℕ) : Finset (Fin n)

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

• Finset.fin n s = Finset.map Fin.equivSubtype.symm.toEmbedding (Finset.subtype (fun (i : ℕ) => i < n) s)

@[simp]

theorem Finset.mem_fin {n : ℕ} {s : Finset ℕ} (a : Fin n) : a ∈ Finset.fin n s ↔ ↑a ∈ s

theorem Finset.fin_mono {n : ℕ} : Monotone (Finset.fin n)

@[simp]

theorem Finset.fin_map {n : ℕ} {s : Finset ℕ} : Finset.map Fin.valEmbedding (Finset.fin n s) = Finset.filter (fun (x : ℕ) => x < n) s

theorem Finset.subset_image_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} : t ⊆ Finset.image f s ↔ ∃ s' ⊆ s, Finset.image f s' = t

If a finset t is a subset of the image of another finset s under f, then it is equal to the image of a subset of s.

For the version where s is a set, see subset_set_image_iff.

theorem Finset.subset_set_image_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Set α} {t : Finset β} {f : α → β} : ↑t ⊆ f '' s ↔ ∃ (s' : Finset α), ↑s' ⊆ s ∧ Finset.image f s' = t

If a Finset is a subset of the image of a Set under f, then it is equal to the Finset.image of a Finset subset of that Set.

theorem Finset.range_sdiff_zero {n : ℕ} : Finset.range (n + 1) \ {0} = Finset.image Nat.succ (Finset.range n)

theorem Multiset.toFinset_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α → β) (m : Multiset α) : (Multiset.map f m).toFinset = Finset.image f m.toFinset

def Equiv.finsetCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) : Finset α ≃ Finset β

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

Equations

• e.finsetCongr = { toFun := fun (s : Finset α) => Finset.map e.toEmbedding s, invFun := fun (s : Finset β) => Finset.map e.symm.toEmbedding s, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.finsetCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Finset α) : e.finsetCongr s = Finset.map e.toEmbedding s

@[simp]

theorem Equiv.finsetCongr_refl {α : Type u_1} : (Equiv.refl α).finsetCongr = Equiv.refl (Finset α)

@[simp]

theorem Equiv.finsetCongr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) : e.finsetCongr.symm = e.symm.finsetCongr

@[simp]

theorem Equiv.finsetCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (e' : β ≃ γ) : e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr

theorem Equiv.finsetCongr_toEmbedding {α : Type u_1} {β : Type u_2} (e : α ≃ β) : e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding