data.finset.image - mathlib3 docs

def finset.map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : finset α) :

When f is an embedding of α in β and s is a finset in α, then s.map f is the image finset in β. The embedding condition guarantees that there are no duplicates in the image.

Equations

finset.map f s = {val := multiset.map ⇑f s.val, nodup := _}

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

finset.map_embedding f = order_embedding.of_map_le_iff (finset.map f) _

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} (p : α → Prop) [decidable_pred p] (f : α ↪ β) (s : finset α) [decidable_pred (λ (b : β), ∃ (a : α), p a ∧ ⇑f a = b)] :

finset.map f (finset.filter p s) = finset.filter (λ (b : β), ∃ (a : α), p a ∧ ⇑f a = b) (finset.map f s)

source

theorem finset.filter_attach' {α : Type u_1} [decidable_eq α] (s : finset α) (p : ↥s → Prop) [decidable_pred p] :

finset.filter p s.attach = finset.map {to_fun := subtype.map id _, inj' := _} (finset.filter (λ (x : α), ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach

source

@[simp]

theorem finset.filter_attach {α : Type u_1} (p : α → Prop) [decidable_pred p] (s : finset α) :

finset.filter (λ (x : {x // x ∈ s}), p ↑x) s.attach = finset.map ((function.embedding.refl α).subtype_map finset.mem_of_mem_filter) (finset.filter p s).attach

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

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

finset.image f s = (multiset.map f s.val).to_finset

Instances for finset.image

finset.can_lift

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

finset.can_lift c p = {prf := _}

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

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

finset.subtype p s = finset.map {to_fun := λ (x : {x // x ∈ finset.filter p s}), ⟨x.val, _⟩, inj' := _} (finset.filter p s).attach

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