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 #

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
source
@[simp]
theorem finset.map_val {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : finset α) :
(finset.map f s).val = multiset.map ⇑f s.val
source
@[simp]
theorem finset.map_empty {α : Type u_1} {β : Type u_2} (f : α ↪ β) :
finset.map f ∅ = ∅
source
@[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
source
@[simp]
theorem finset.mem_map_equiv {α : Type u_1} {β : Type u_2} {s : finset α} {f : α ≃ β} {b : β} :
b ∈ finset.map f.to_embedding s ↔ ⇑(f.symm) b ∈ s
source
theorem finset.mem_map' {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : finset α} :
⇑f a ∈ finset.map f s ↔ a ∈ s
source
theorem finset.mem_map_of_mem {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : finset α} :
a ∈ s → ⇑f a ∈ finset.map f s
source
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) _
source
theorem finset.apply_coe_mem_map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : finset α) (x : ↥s) :
⇑f ↑x ∈ finset.map f s
source
@[simp, norm_cast]
theorem finset.coe_map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : finset α) :
↑(finset.map f s) = ⇑f '' ↑s
source
theorem finset.coe_map_subset_range {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : finset α) :
↑(finset.map f s) ⊆ set.range ⇑f
source
theorem finset.map_perm {α : Type u_1} {s : finset α} {σ : equiv.perm α} (hs : {a : α | ⇑σ a ≠ a} ⊆ ↑s) :
finset.map ↑σ s = s

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

source
theorem finset.map_to_finset {α : Type u_1} {β : Type u_2} {f : α ↪ β} [decidable_eq α] [decidable_eq β] {s : multiset α} :
finset.map f s.to_finset = (multiset.map ⇑f s).to_finset
source
@[simp]
theorem finset.map_refl {α : Type u_1} {s : finset α} :
finset.map (function.embedding.refl α) s = s
source
@[simp]
theorem finset.map_cast_heq {α β : Type u_1} (h : α = β) (s : finset α) :
finset.map (equiv.cast h).to_embedding s == s
source
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
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)) :
finset.map f (finset.map g s) = finset.map g' (finset.map f' s)
source
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)
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 α} :
finset.map f s₁ ⊆ finset.map f s₂ ↔ s₁ ⊆ s₂
source
def finset.map_embedding {α : 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
source
@[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₂
source
theorem finset.map_injective {α : Type u_1} {β : Type u_2} (f : α ↪ β) :
function.injective (finset.map f)
source
@[simp]
theorem finset.map_embedding_apply {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : finset α} :
⇑(finset.map_embedding f) s = finset.map f s
source
theorem finset.filter_map {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : finset α} {p : β → Prop} [decidable_pred p] :
finset.filter p (finset.map f s) = finset.map f (finset.filter (p ∘ ⇑f) s)
source
theorem finset.map_filter {α : Type u_1} {β : Type u_2} {s : finset α} {f : α ≃ β} {p : α → Prop} [decidable_pred p] :
finset.map f.to_embedding (finset.filter p s) = finset.filter (p ∘ ⇑(f.symm)) (finset.map f.to_embedding s)
source
@[simp]
theorem finset.disjoint_map {α : Type u_1} {β : Type u_2} {s t : finset α} (f : α ↪ β) :
disjoint (finset.map f s) (finset.map f t) ↔ disjoint s t
source
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'
source
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.

source
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₂
source
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₂
source
@[simp]
theorem finset.map_singleton {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : α) :
finset.map f {a} = {⇑f a}
source
@[simp]
theorem finset.map_insert {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α ↪ β) (a : α) (s : finset α) :
finset.map f (has_insert.insert a s) = has_insert.insert (⇑f a) (finset.map f s)
source
@[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) _
source
@[simp]
theorem finset.map_eq_empty {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : finset α} :
finset.map f s = ∅ ↔ s = ∅
source
@[simp]
theorem finset.map_nonempty {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : finset α} :
(finset.map f s).nonempty ↔ s.nonempty
source
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.

source
theorem finset.attach_map_val {α : Type u_1} {s : finset α} :
finset.map (function.embedding.subtype (λ (x : α), x ∈ s)) s.attach = s
source
theorem finset.disjoint_range_add_left_embedding (a b : ℕ) :
disjoint (finset.range a) (finset.map (add_left_embedding a) (finset.range b))
source
theorem finset.disjoint_range_add_right_embedding (a b : ℕ) :
disjoint (finset.range a) (finset.map (add_right_embedding a) (finset.range b))
source
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)) _
source
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)) _
source
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 #

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

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

Equations
Instances for finset.image
source
@[simp]
theorem finset.image_val {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) (s : finset α) :
(finset.image f s).val = (multiset.map f s.val).dedup
source
@[simp]
theorem finset.image_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) :
finset.image f ∅ = ∅
source
@[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
source
theorem finset.mem_image_of_mem {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (f : α → β) {a : α} (h : a ∈ s) :
f a ∈ finset.image f s
source
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)
source
@[simp]
theorem finset.mem_image_const {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {b c : β} :
c ∈ finset.image (function.const α b) s ↔ s.nonempty ∧ b = c
source
theorem finset.mem_image_const_self {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {b : β} :
b ∈ finset.image (function.const α b) s ↔ s.nonempty
source
@[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
source
theorem finset.image_congr {α : Type u_1} {β : Type u_2} [decidable_eq β] {f g : α → β} {s : finset α} (h : set.eq_on f g ↑s) :
finset.image f s = finset.image g s
source
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
source
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
source
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
source
@[simp, norm_cast]
theorem finset.coe_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {f : α → β} :
↑(finset.image f s) = f '' ↑s
source
@[protected]
theorem finset.nonempty.image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (h : s.nonempty) (f : α → β) :
(finset.image f s).nonempty
source
@[simp]
theorem finset.nonempty.image_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (f : α → β) :
(finset.image f s).nonempty ↔ s.nonempty
source
theorem finset.image_to_finset {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} [decidable_eq α] {s : multiset α} :
finset.image f s.to_finset = (multiset.map f s).to_finset
source
theorem finset.image_val_of_inj_on {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} (H : set.inj_on f ↑s) :
(finset.image f s).val = multiset.map f s.val
source
@[simp]
theorem finset.image_id {α : Type u_1} {s : finset α} [decidable_eq α] :
finset.image id s = s
source
@[simp]
theorem finset.image_id' {α : Type u_1} {s : finset α} [decidable_eq α] :
finset.image (λ (x : α), x) s = s
source
theorem finset.image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] {f : α → β} {s : finset α} [decidable_eq γ] {g : β → γ} :
finset.image g (finset.image f s) = finset.image (g ∘ f) s
source
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)) :
finset.image f (finset.image g s) = finset.image g' (finset.image f' s)
source
theorem function.semiconj.finset_image {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α → β} {ga : α → α} {gb : β → β} (h : function.semiconj f ga gb) :
function.semiconj (finset.image f) (finset.image ga) (finset.image gb)
source
theorem function.commute.finset_image {α : Type u_1} [decidable_eq α] {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} [decidable_eq β] {f : α → β} {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) :
finset.image f s₁ ⊆ finset.image f s₂
source
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
source
theorem finset.image_mono {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) :
monotone (finset.image f)
source
theorem finset.image_subset_image_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s t : finset α} (hf : function.injective f) :
finset.image f s ⊆ finset.image f t ↔ s ⊆ t
source
theorem finset.coe_image_subset_range {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :
↑(finset.image f s) ⊆ set.range f
source
theorem finset.image_filter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} {p : β → Prop} [decidable_pred p] :
finset.filter p (finset.image f s) = finset.image f (finset.filter (p ∘ f) s)
source
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₂
source
theorem finset.image_inter_subset {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α → β) (s t : finset α) :
finset.image f (s ∩ t) ⊆ finset.image f s ∩ finset.image f t
source
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)) :
finset.image f (s ∩ t) = finset.image f s ∩ finset.image f t
source
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₂
source
@[simp]
theorem finset.image_singleton {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) (a : α) :
finset.image f {a} = {f a}
source
@[simp]
theorem finset.image_insert {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α → β) (a : α) (s : finset α) :
finset.image f (has_insert.insert a s) = has_insert.insert (f a) (finset.image f s)
source
theorem finset.erase_image_subset_image_erase {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α → β) (s : finset α) (a : α) :
(finset.image f s).erase (f a) ⊆ finset.image f (s.erase a)
source
@[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)
source
@[simp]
theorem finset.image_eq_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :
finset.image f s = ∅ ↔ s = ∅
source
theorem finset.image_sdiff {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α → β} (s t : finset α) (hf : function.injective f) :
finset.image f (s \ t) = finset.image f s \ finset.image f t
source
theorem finset.image_symm_diff {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α → β} (s t : finset α) (hf : function.injective f) :
finset.image f (s ∆ t) = finset.image f s ∆ finset.image f t
source
@[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)) :
disjoint s t
source
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)
source
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)
source
theorem finset.range_add (a b : ℕ) :
finset.range (a + b) = finset.range a ∪ finset.map (add_left_embedding a) (finset.range b)
source
@[simp]
theorem finset.attach_image_val {α : Type u_1} [decidable_eq α] {s : finset α} :
finset.image subtype.val s.attach = s
source
@[simp]
theorem finset.attach_image_coe {α : Type u_1} [decidable_eq α] {s : finset α} :
finset.image coe s.attach = s
source
@[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)
source
theorem finset.map_eq_image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α ↪ β) (s : finset α) :
finset.map f s = finset.image ⇑f s
source
@[simp]
theorem finset.disjoint_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s t : finset α} {f : α → β} (hf : function.injective f) :
disjoint (finset.image f s) (finset.image f t) ↔ disjoint s t
source
theorem finset.image_const {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (h : s.nonempty) (b : β) :
finset.image (λ (a : α), b) s = {b}
source
@[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)
source
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))
source
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))
source
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
source
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 #

source
@[protected]
def finset.subtype {α : Type u_1} (p : α → Prop) [decidable_pred 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
source
@[simp]
theorem finset.mem_subtype {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} {a : subtype p} :
a ∈ finset.subtype p s ↔ ↑a ∈ s
source
theorem finset.subtype_eq_empty {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} :
finset.subtype p s = ∅ ↔ ∀ (x : α), p x → x ∉ s
source
theorem finset.subtype_mono {α : Type u_1} {p : α → Prop} [decidable_pred p] :
monotone (finset.subtype p)
source
@[simp]
theorem finset.subtype_map {α : Type u_1} (p : α → Prop) [decidable_pred 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.

source
theorem finset.subtype_map_of_mem {α : Type u_1} {p : α → Prop} [decidable_pred 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.

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

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

source
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 #

source
@[protected]
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
source
@[simp]
theorem finset.mem_fin {n : ℕ} {s : finset ℕ} (a : fin n) :
a ∈ finset.fin n s ↔ ↑a ∈ s
source
theorem finset.fin_mono {n : ℕ} :
monotone (finset.fin n)
source
@[simp]
theorem finset.fin_map {n : ℕ} {s : finset ℕ} :
finset.map fin.coe_embedding (finset.fin n s) = finset.filter (λ (_x : ℕ), _x < n) s
source
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
source
theorem finset.range_sdiff_zero {n : ℕ} :
finset.range (n + 1) \ {0} = finset.image nat.succ (finset.range n)
source
theorem multiset.to_finset_map {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α → β) (m : multiset α) :
(multiset.map f m).to_finset = finset.image f m.to_finset
source
@[protected]
def equiv.finset_congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
finset α ≃ finset β

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

Equations
source
@[simp]
theorem equiv.finset_congr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : finset α) :
⇑(e.finset_congr) s = finset.map e.to_embedding s
source
@[simp]
theorem equiv.finset_congr_refl {α : Type u_1} :
(equiv.refl α).finset_congr = equiv.refl (finset α)
source
@[simp]
theorem equiv.finset_congr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
e.finset_congr.symm = e.symm.finset_congr
source
@[simp]
theorem equiv.finset_congr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (e' : β ≃ γ) :
e.finset_congr.trans e'.finset_congr = (e.trans e').finset_congr
source
theorem equiv.finset_congr_to_embedding {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
e.finset_congr.to_embedding = (finset.map_embedding e.to_embedding).to_embedding