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.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

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 := (_ : Multiset.Nodup (Multiset.map (↑f) s.val)) }

@[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, a ∈ s ∧ ↑f a = b

@[simp]

theorem Finset.mem_map_equiv {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {b : β} : b ∈ Finset.map (Equiv.toEmbedding f) 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) (_ : ↑f x ∈ Finset.map f s)

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 (Multiset.toFinset s) = Multiset.toFinset (Multiset.map (↑f) s)

@[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.toEmbedding (Equiv.cast h)) 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 (Function.Embedding.trans f 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₂

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) (_ : ∀ (x x_1 : Finset α), Finset.map f x ⊆ Finset.map f x_1 ↔ x ⊆ x_1)

@[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.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} {s : Finset α} {f : α ≃ β} {p : α → Prop} [DecidablePred p] : Finset.map (Equiv.toEmbedding f) (Finset.filter p s) = Finset.filter (p ∘ ↑f.symm) (Finset.map (Equiv.toEmbedding f) 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₂)) (_ : Disjoint (Finset.map f s₁) (Finset.map f s₂))) : Finset.map f (Finset.disjUnion s₁ s₂ h) = Finset.disjUnion (Finset.map f s₁) (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₂) (_ : Disjoint s₁ s₂)) : Finset.map f (Finset.disjUnion s₁ s₂ h) = Finset.disjUnion (Finset.map f s₁) (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) (_ : ¬↑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.Nonempty (Finset.map f s) ↔ Finset.Nonempty s

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

Alias of the reverse direction of Finset.map_nonempty.

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

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

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

theorem Finset.map_disjiUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α ↪ β} {s : Finset α} {t : β → Finset γ} {h : Set.PairwiseDisjoint (↑(Finset.map f s)) t} : Finset.disjiUnion (Finset.map f s) t h = Finset.disjiUnion s (fun a => t (↑f a)) fun x ha x_1 hb hab => h (↑f x) (_ : ↑f x ∈ Finset.map f s) (↑f x_1) (_ : ↑f x_1 ∈ Finset.map f s) (_ : ↑f x ≠ ↑f x_1)

theorem Finset.disjiUnion_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : α → Finset β} {f : β ↪ γ} {h : Set.PairwiseDisjoint (↑s) t} : Finset.map f (Finset.disjiUnion s t h) = Finset.disjiUnion s (fun a => Finset.map f (t a)) (_ : ∀ (a : α), a ∈ ↑s → ∀ (b : α), b ∈ ↑s → a ≠ b → Disjoint ((fun a => Finset.map f (t a)) a) ((fun a => Finset.map f (t a)) b))

theorem Finset.range_add_one' (n : ℕ) : Finset.range (n + 1) = insert 0 (Finset.map { toFun := fun i => i + 1, inj' := (_ : ∀ (i j : ℕ), i + 1 = j + 1 → i = j) } (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.toFinset (Multiset.map f s.val)

@[simp]

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

@[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, 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 : β) → b ∈ Finset.image f s → p b) ↔ (a : α) → 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 ↔ Finset.Nonempty s ∧ 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 ↔ Finset.Nonempty s

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

Equations

• @Finset.canLift = @Finset.canLift.proof_1

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

theorem Finset.filter_mem_image_eq_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Finset α) (t : Finset β) (h : ∀ (x : α), 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.Nonempty (Finset.filter (fun x => f x = y) s) ↔ y ∈ Finset.image f s

@[simp]

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

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

@[simp]

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

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

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 : α), 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.image_filter {α : 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)

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.erase (Finset.image f s) (f a) ⊆ Finset.image f (Finset.erase s 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 (Finset.erase s a) = Finset.erase (Finset.image f s) (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 (s ∆ t) = 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 (Finset.attach s) = s

@[simp]

theorem Finset.attach_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} : Finset.attach (insert a s) = insert { val := a, property := (_ : a ∈ insert a s) } (Finset.image (fun x => { val := ↑x, property := (_ : ↑x ∈ insert a s) }) (Finset.attach s))

@[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 : Finset.Nonempty s) (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 (Finset.erase s a) = Finset.erase (Finset.map f s) (↑f a)

theorem Finset.image_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {f : α → β} {s : Finset α} {t : β → Finset γ} : Finset.biUnion (Finset.image f s) t = Finset.biUnion s 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 (Finset.biUnion s t) = Finset.biUnion s 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.biUnion (Finset.image g s) 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 : α → β} : (Finset.biUnion s fun a => {f a}) = Finset.image f s

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

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

@[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 : α) → 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 (Equiv.toEmbedding Fin.equivSubtype.symm) (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 : Set α} {t : Finset β} {f : α → β} : ↑t ⊆ f '' s ↔ ∃ s', ↑s' ⊆ s ∧ Finset.image f s' = t

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.toFinset (Multiset.map f m) = Finset.image f (Multiset.toFinset m)

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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