# 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 `none`s.
- `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`.

### map #

source
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 := ⋯ }

Instances For

source
@[simp]
theorem Finset.map_val {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) :
(map f s).val = Multiset.map (⇑f) s.val
source
@[simp]
theorem Finset.map_empty {α : Type u_1} {β : Type u_2} (f : α ↪ β) :
map f ∅ = ∅
source
@[simp]
theorem Finset.mem_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {b : β} :
b ∈ map f s ↔ ∃ a ∈ s, f a = b
source
@[simp]
theorem Finset.mem_map_equiv {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {b : β} :
b ∈ map f.toEmbedding s ↔ f.symm b ∈ s
source
@[simp]
theorem Finset.mem_map' {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : Finset α} :
f a ∈ map f s ↔ a ∈ s
source
@[simp]
theorem Finset.mem_map_mk {α : Type u_1} {β : Type u_2} (f : α → β) {a : α} {s : Finset α} (hf : Function.Injective f) :
f a ∈ map { toFun := f, inj' := hf } s ↔ a ∈ s
source
theorem Finset.mem_map_of_mem {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : Finset α} :
a ∈ s → f a ∈ map f s
source
theorem Finset.forall_mem_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {p : (a : β) → a ∈ map f s → Prop} :
(∀ (y : β) (H : y ∈ map f s), p y H) ↔ ∀ (x : α) (H : x ∈ s), p (f x) ⋯
source
theorem Finset.apply_coe_mem_map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) (x : ↥s) :
f ↑x ∈ map f s
source
@[simp]
theorem Finset.coe_map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) :
↑(map f s) = ⇑f '' ↑s
source
theorem Finset.coe_map_subset_range {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) :
↑(map f s) ⊆ Set.range ⇑f
source
theorem Finset.map_perm {α : Type u_1} {s : Finset α} {σ : Equiv.Perm α} (hs : {a : α | σ a ≠ a} ⊆ ↑s) :
map (Equiv.toEmbedding σ) s = s

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

source
theorem Finset.map_toFinset {α : Type u_1} {β : Type u_2} {f : α ↪ β} [DecidableEq α] [DecidableEq β] {s : Multiset α} :
map f s.toFinset = (Multiset.map (⇑f) s).toFinset
source
@[simp]
theorem Finset.map_refl {α : Type u_1} {s : Finset α} :
map (Function.Embedding.refl α) s = s
source
@[simp]
theorem Finset.map_cast_heq {α β : Type u_4} (h : α = β) (s : Finset α) :
map (Equiv.cast h).toEmbedding s ≍ s
source
theorem Finset.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ↪ β) (g : β ↪ γ) (s : Finset α) :
map g (map f s) = map (f.trans g) s
source
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)) :
map f (map g s) = map g' (map f' s)
source
theorem Function.Semiconj.finset_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {ga : α ↪ α} {gb : β ↪ β} (h : Semiconj ⇑f ⇑ga ⇑gb) :
Semiconj (Finset.map f) (Finset.map ga) (Finset.map gb)
source
theorem Function.Commute.finset_map {α : Type u_1} {f g : α ↪ α} (h : Function.Commute ⇑f ⇑g) :
Function.Commute (Finset.map f) (Finset.map g)
source
@[simp]
theorem Finset.map_subset_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : Finset α} :
map f s₁ ⊆ map f s₂ ↔ s₁ ⊆ s₂
source
theorem GCongr.finsetMap_subset {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : Finset α} :
s₁ ⊆ s₂ → Finset.map f s₁ ⊆ Finset.map f s₂

Alias of the reverse direction of `Finset.map_subset_map`.

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

The `Finset` version of `Equiv.subset_symm_image`.

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

The `Finset` version of `Equiv.symm_image_subset`.

source
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) ⋯

Instances For

source
@[simp]
theorem Finset.map_inj {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : Finset α} :
map f s₁ = map f s₂ ↔ s₁ = s₂
source
theorem Finset.map_injective {α : Type u_1} {β : Type u_2} (f : α ↪ β) :
Function.Injective (map f)
source
@[simp]
theorem Finset.map_ssubset_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s t : Finset α} :
map f s ⊂ map f t ↔ s ⊂ t
source
theorem GCongr.finsetMap_ssubset {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s t : Finset α} :
s ⊂ t → Finset.map f s ⊂ Finset.map f t

Alias of the reverse direction of `Finset.map_ssubset_map`.

source
@[simp]
theorem Finset.mapEmbedding_apply {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} :
(mapEmbedding f) s = map f s
source
theorem Finset.filter_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {p : β → Prop} [DecidablePred p] :
filter p (map f s) = map f (filter (p ∘ ⇑f) s)
source
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] :
map f (filter p s) = {b ∈ map f s | ∃ (a : α), p a ∧ f a = b}
source
theorem Finset.filter_attach' {α : Type u_1} [DecidableEq α] (s : Finset α) (p : ↥s → Prop) [DecidablePred p] :
filter p s.attach = map { toFun := Subtype.map id ⋯, inj' := ⋯ } {x ∈ s | ∃ (h : x ∈ s), p ⟨x, h⟩}.attach
source
theorem Finset.filter_attach {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) :
{a ∈ s.attach | p ↑a} = map ((Function.Embedding.refl α).subtypeMap ⋯) (filter p s).attach
source
theorem Finset.map_filter {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {p : α → Prop} [DecidablePred p] :
map f.toEmbedding (filter p s) = filter (p ∘ ⇑f.symm) (map f.toEmbedding s)
source
@[simp]
theorem Finset.disjoint_map {α : Type u_1} {β : Type u_2} {s t : Finset α} (f : α ↪ β) :
Disjoint (map f s) (map f t) ↔ Disjoint s t
source
theorem Finset.map_disjUnion {α : Type u_1} {β : Type u_2} {f : α ↪ β} (s₁ s₂ : Finset α) (h : Disjoint s₁ s₂) (h' : Disjoint (map f s₁) (map f s₂) := ⋯) :
map f (s₁.disjUnion s₂ h) = (map f s₁).disjUnion (map f s₂) h'
source
theorem Finset.map_disjUnion' {α : Type u_1} {β : Type u_2} {f : α ↪ β} (s₁ s₂ : Finset α) (h' : Disjoint (map f s₁) (map f s₂)) (h : Disjoint s₁ s₂ := ⋯) :
map f (s₁.disjUnion s₂ h) = (map f s₁).disjUnion (map f s₂) h'

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

source
theorem Finset.map_union {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) :
map f (s₁ ∪ s₂) = map f s₁ ∪ map f s₂
source
theorem Finset.map_inter {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) :
map f (s₁ ∩ s₂) = map f s₁ ∩ map f s₂
source
theorem Finset.map_sdiff {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) :
map f (s₁ \ s₂) = map f s₁ \ map f s₂
source
@[simp]
theorem Finset.map_singleton {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : α) :
map f {a} = {f a}
source
@[simp]
theorem Finset.map_insert {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α ↪ β) (a : α) (s : Finset α) :
map f (insert a s) = insert (f a) (map f s)
source
@[simp]
theorem Finset.map_cons {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : α) (s : Finset α) (ha : a ∉ s) :
map f (cons a s ha) = cons (f a) (map f s) ⋯
source
@[simp]
theorem Finset.map_eq_empty {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} :
map f s = ∅ ↔ s = ∅
source
@[simp]
theorem Finset.map_nonempty {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} :
(map f s).Nonempty ↔ s.Nonempty
source
theorem Finset.Nonempty.map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} :
s.Nonempty → (map f s).Nonempty

Alias of the reverse direction of `Finset.map_nonempty`.

source
@[simp]
theorem Finset.map_nontrivial {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} :
(map f s).Nontrivial ↔ s.Nontrivial
source
theorem Finset.attach_map_val {α : Type u_1} {s : Finset α} :
map (Function.Embedding.subtype fun (x : α) => x ∈ s) s.attach = s
source
theorem Finset.range_add_one' (n : ℕ) :
range (n + 1) = insert 0 (map { toFun := fun (i : ℕ) => i + 1, inj' := ⋯ } (range n))

### image #

source
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

Instances For

source
@[simp]
theorem Finset.image_val {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Finset α) :
(image f s).val = (Multiset.map f s.val).dedup
source
@[simp]
theorem Finset.image_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) :
image f ∅ = ∅
source
@[simp]
theorem Finset.mem_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {b : β} :
b ∈ image f s ↔ ∃ a ∈ s, f a = b
source
theorem Finset.mem_image_of_mem {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (f : α → β) {a : α} (h : a ∈ s) :
f a ∈ image f s
source
theorem Finset.forall_mem_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop} :
(∀ y ∈ image f s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)
source
theorem Finset.exists_mem_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop} :
(∃ y ∈ image f s, p y) ↔ ∃ x ∈ s, p (f x)
source
theorem Finset.map_eq_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α ↪ β) (s : Finset α) :
map f s = image (⇑f) s
source
theorem Finset.mem_image_const {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {b c : β} :
c ∈ image (Function.const α b) s ↔ s.Nonempty ∧ b = c
source
theorem Finset.mem_image_const_self {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {b : β} :
b ∈ image (Function.const α b) s ↔ s.Nonempty
source
instance Finset.canLift {α : Type u_1} {β : Type u_2} [DecidableEq β] (c : α → β) (p : β → Prop) [CanLift β α c p] :
CanLift (Finset β) (Finset α) (image c) fun (s : Finset β) => ∀ x ∈ s, p x
source
theorem Finset.image_congr {α : Type u_1} {β : Type u_2} [DecidableEq β] {f g : α → β} {s : Finset α} (h : Set.EqOn f g ↑s) :
image f s = image g s
source
theorem Function.Injective.mem_finset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {a : α} (hf : Injective f) :
f a ∈ Finset.image f s ↔ a ∈ s
source
@[simp]
theorem Finset.coe_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} :
↑(image f s) = f '' ↑s
source
@[simp]
theorem Finset.image_nonempty {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} :
(image f s).Nonempty ↔ s.Nonempty
source
theorem Finset.Nonempty.image {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (h : s.Nonempty) (f : α → β) :
(image f s).Nonempty
source
theorem Finset.Nonempty.of_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} :
(image f s).Nonempty → s.Nonempty

Alias of the forward direction of `Finset.image_nonempty`.

source
theorem Finset.image_toFinset {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} [DecidableEq α] {s : Multiset α} :
image f s.toFinset = (Multiset.map f s).toFinset
source
theorem Finset.image_val_of_injOn {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} (H : Set.InjOn f ↑s) :
(image f s).val = Multiset.map f s.val
source
@[simp]
theorem Finset.image_id {α : Type u_1} {s : Finset α} [DecidableEq α] :
image id s = s
source
@[simp]
theorem Finset.image_id' {α : Type u_1} {s : Finset α} [DecidableEq α] :
image (fun (x : α) => x) s = s
source
theorem Finset.image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] {f : α → β} {s : Finset α} [DecidableEq γ] {g : β → γ} :
image g (image f s) = image (g ∘ f) s
source
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)) :
image f (image g s) = image g' (image f' s)
source
theorem Function.Semiconj.finset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) :
Semiconj (Finset.image f) (Finset.image ga) (Finset.image gb)
source
theorem Function.Commute.finset_image {α : Type u_1} [DecidableEq α] {f g : α → α} (h : Function.Commute f g) :
Function.Commute (Finset.image f) (Finset.image g)
source
theorem Finset.image_subset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) :
image f s₁ ⊆ image f s₂
source
theorem Finset.image_subset_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} :
image f s ⊆ t ↔ ∀ x ∈ s, f x ∈ t
source
theorem Finset.image_mono {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) :
Monotone (image f)
source
theorem Finset.image_injective {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} (hf : Function.Injective f) :
Function.Injective (image f)
source
theorem Finset.image_inj {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s t : Finset α} (hf : Function.Injective f) :
image f s = image f t ↔ s = t
source
theorem Finset.image_subset_image_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s t : Finset α} (hf : Function.Injective f) :
image f s ⊆ image f t ↔ s ⊆ t
source
theorem Finset.image_ssubset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s t : Finset α} (hf : Function.Injective f) :
image f s ⊂ image f t ↔ s ⊂ t
source
theorem Finset.coe_image_subset_range {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} :
↑(image f s) ⊆ Set.range f
source
theorem Finset.filter_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop} [DecidablePred p] :
filter p (image f s) = image f ({a ∈ s | p (f a)})
source
theorem Finset.fiber_nonempty_iff_mem_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {y : β} :
{x ∈ s | f x = y}.Nonempty ↔ y ∈ image f s
source
theorem Finset.image_union {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : α → β} (s₁ s₂ : Finset α) :
image f (s₁ ∪ s₂) = image f s₁ ∪ image f s₂
source
theorem Finset.image_inter_subset {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : α → β) (s t : Finset α) :
image f (s ∩ t) ⊆ image f s ∩ image f t
source
theorem Finset.image_inter_of_injOn {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Set.InjOn f (↑s ∪ ↑t)) :
image f (s ∩ t) = image f s ∩ image f t
source
theorem Finset.image_inter {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} [DecidableEq α] (s₁ s₂ : Finset α) (hf : Function.Injective f) :
image f (s₁ ∩ s₂) = image f s₁ ∩ image f s₂
source
@[simp]
theorem Finset.image_singleton {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (a : α) :
image f {a} = {f a}
source
@[simp]
theorem Finset.image_insert {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : α → β) (a : α) (s : Finset α) :
image f (insert a s) = insert (f a) (image f s)
source
theorem Finset.erase_image_subset_image_erase {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : α → β) (s : Finset α) (a : α) :
(image f s).erase (f a) ⊆ image f (s.erase a)
source
@[simp]
theorem Finset.image_erase {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : α → β} (hf : Function.Injective f) (s : Finset α) (a : α) :
image f (s.erase a) = (image f s).erase (f a)
source
@[simp]
theorem Finset.image_eq_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} :
image f s = ∅ ↔ s = ∅
source
theorem Finset.image_sdiff {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Function.Injective f) :
image f (s \ t) = image f s \ image f t
source
theorem Finset.image_sdiff_of_injOn {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} [DecidableEq α] {t : Finset α} (hf : Set.InjOn f ↑s) (hts : t ⊆ s) :
image f (s \ t) = image f s \ image f t
source
theorem Disjoint.of_image_finset {α : Type u_1} {β : Type u_2} [DecidableEq β] {s t : Finset α} {f : α → β} (h : Disjoint (Finset.image f s) (Finset.image f t)) :
Disjoint s t
source
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 ∈ image (fun (i : ℕ) => f i) (range n)
source
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 ∈ image (fun (i : ℕ) => f ↑i) (range n)
source
@[simp]
theorem Finset.attach_image_val {α : Type u_1} [DecidableEq α] {s : Finset α} :
image Subtype.val s.attach = s
source
@[simp]
theorem Finset.attach_cons {α : Type u_1} (a : α) (s : Finset α) (ha : a ∉ s) :
(cons a s ha).attach = cons ⟨a, ⋯⟩ (map { toFun := fun (x : { x : α // x ∈ s }) => ⟨↑x, ⋯⟩, inj' := ⋯ } s.attach) ⋯
source
@[simp]
theorem Finset.attach_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
(insert a s).attach = insert ⟨a, ⋯⟩ (image (fun (x : { x : α // x ∈ s }) => ⟨↑x, ⋯⟩) s.attach)
source
@[simp]
theorem Finset.disjoint_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {s t : Finset α} {f : α → β} (hf : Function.Injective f) :
Disjoint (image f s) (image f t) ↔ Disjoint s t
source
theorem Finset.image_const {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (h : s.Nonempty) (b : β) :
image (fun (x : α) => b) s = {b}
source
@[simp]
theorem Finset.map_erase {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : α ↪ β) (s : Finset α) (a : α) :
map f (s.erase a) = (map f s).erase (f a)

### filterMap #

source
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 := ⋯ }

Instances For

source
@[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'} :
(filterMap f s' f_inj).val = Multiset.filterMap f s'.val
source
@[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'} :
filterMap f ∅ f_inj = ∅
source
@[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 ∈ filterMap f s f_inj ↔ ∃ a ∈ s, f a = some b
source
@[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'} :
↑(filterMap f s f_inj) = {b : β | ∃ a ∈ s, f a = some b}
source
@[simp]
theorem Finset.filterMap_some {α : Type u_1} {s : Finset α} :
filterMap some s ⋯ = s
source
theorem Finset.filterMap_mono {α : Type u_1} {β : Type u_2} (f : α → Option β) {s t : Finset α} {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'} (h : s ⊆ t) :
filterMap f s f_inj ⊆ filterMap f t f_inj
source
theorem List.toFinset_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) [DecidableEq α] [DecidableEq β] (f_inj : ∀ (a a' : α) (b : β), f a = some b → f a' = some b → a = a') (s : List α) :
(filterMap f s).toFinset = Finset.filterMap f s.toFinset f_inj

### Subtype #

source
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

Instances For

source
@[simp]
theorem Finset.mem_subtype {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} {a : Subtype p} :
a ∈ Finset.subtype p s ↔ ↑a ∈ s
source
theorem Finset.subtype_eq_empty {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} :
Finset.subtype p s = ∅ ↔ ∀ (x : α), p x → x ∉ s
source
theorem Finset.subtype_mono {α : Type u_1} {p : α → Prop} [DecidablePred p] :
Monotone (Finset.subtype p)
source
@[simp]
theorem Finset.subtype_map {α : Type u_1} (p : α → Prop) [DecidablePred p] {s : Finset α} :
map (Function.Embedding.subtype p) (Finset.subtype p s) = filter p s

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

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

source
theorem Finset.property_of_mem_map_subtype {α : Type u_1} {p : α → Prop} (s : Finset { x : α // p x }) {a : α} (h : a ∈ 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.

source
theorem Finset.notMem_map_subtype_of_not_property {α : Type u_1} {p : α → Prop} (s : Finset { x : α // p x }) {a : α} (h : ¬p a) :
a ∉ 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.

source
@[deprecated Finset.notMem_map_subtype_of_not_property (since := "2025-05-23")]
theorem Finset.not_mem_map_subtype_of_not_property {α : Type u_1} {p : α → Prop} (s : Finset { x : α // p x }) {a : α} (h : ¬p a) :
a ∉ map (Function.Embedding.subtype fun (x : α) => p x) s

Alias of `Finset.notMem_map_subtype_of_not_property`.

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.

source
theorem Finset.map_subtype_subset {α : Type u_1} {t : Set α} (s : Finset ↑t) :
↑(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.

source
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 ∧ 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`.

source
theorem Finset.subset_image_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} :
t ⊆ image f s ↔ ∃ s' ⊆ s, 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`.

source
theorem Finset.subset_univ_image_iff {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {t : Finset β} {f : α → β} :
t ⊆ image f univ ↔ ∃ (s' : Finset α), image f s' = t

A special case of `subset_image_iff`, which corresponds to `Set.subset_range_iff_exists_image_eq` for `Set`.

source
theorem Finset.range_sdiff_zero {n : ℕ} :
range (n + 1) \ {0} = image Nat.succ (range n)
source
theorem Multiset.toFinset_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α → β) (m : Multiset α) :
(map f m).toFinset = Finset.image f m.toFinset
source
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 := ⋯ }

Instances For

source
@[simp]
theorem Equiv.finsetCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Finset α) :
e.finsetCongr s = Finset.map e.toEmbedding s
source
@[simp]
theorem Equiv.finsetCongr_refl {α : Type u_1} :
(Equiv.refl α).finsetCongr = Equiv.refl (Finset α)
source
@[simp]
theorem Equiv.finsetCongr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
e.finsetCongr.symm = e.symm.finsetCongr
source
@[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
source
theorem Equiv.finsetCongr_toEmbedding {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding
source
def Equiv.finsetSubtypeComm {α : Type u_1} (p : α → Prop) :
Finset { a : α // p a } ≃ { s : Finset α // ∀ a ∈ s, p a }

Given a predicate `p : α → Prop`, produces an equivalence between `Finset {a : α // p a}` and `{s : Finset α // ∀ a ∈ s, p a}`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Equiv.finsetSubtypeComm_apply_coe {α : Type u_1} (p : α → Prop) (s : Finset { a : α // p a }) :
↑((Equiv.finsetSubtypeComm p) s) = Finset.map { toFun := fun (a : { a : α // p a }) => ↑a, inj' := ⋯ } s
source
@[simp]
theorem Equiv.finsetSubtypeComm_symm_apply {α : Type u_1} (p : α → Prop) (s : { s : Finset α // ∀ a ∈ s, p a }) :
(Equiv.finsetSubtypeComm p).symm s = Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach