Documentation

Mathlib.Data.Finset.Image

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 #

TODO #

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

map #

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

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
Instances For
    @[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 : α β) :
    @[simp]
    theorem Finset.mem_map {α : Type u_1} {β : Type u_2} {f : α β} {s : Finset α} {b : β} :
    b Finset.map f s as, f a = b
    @[simp]
    theorem Finset.mem_map_equiv {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α β} {b : β} :
    b Finset.map f.toEmbedding s f.symm b s
    @[simp]
    theorem Finset.mem_map' {α : Type u_1} {β : Type u_2} (f : α β) {a : α} {s : Finset α} :
    f a Finset.map f s a s
    theorem Finset.mem_map_of_mem {α : Type u_1} {β : Type u_2} (f : α β) {a : α} {s : Finset α} :
    a sf 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 sProp} :
    (∀ (y : β) (H : y Finset.map f s), p y H) ∀ (x : α) (H : x s), p (f x)
    theorem Finset.apply_coe_mem_map {α : Type u_1} {β : Type u_2} (f : α β) (s : Finset α) (x : { x : α // x s }) :
    f x Finset.map f s
    @[simp]
    theorem Finset.coe_map {α : Type u_1} {β : Type u_2} (f : α β) (s : Finset α) :
    (Finset.map f s) = f '' s
    theorem Finset.coe_map_subset_range {α : Type u_1} {β : Type u_2} (f : α β) (s : Finset α) :
    (Finset.map f s) Set.range f
    theorem Finset.map_perm {α : Type u_1} {s : Finset α} {σ : Equiv.Perm α} (hs : {a : α | σ a a} s) :

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

    theorem Finset.map_toFinset {α : Type u_1} {β : Type u_2} {f : α β} [DecidableEq α] [DecidableEq β] {s : Multiset α} :
    Finset.map f s.toFinset = (Multiset.map (⇑f) s).toFinset
    @[simp]
    theorem Finset.map_refl {α : Type u_1} {s : Finset α} :
    @[simp]
    theorem Finset.map_cast_heq {α : Type u_4} {β : Type u_4} (h : α = β) (s : Finset α) :
    HEq (Finset.map (Equiv.cast h).toEmbedding s) s
    theorem Finset.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : β γ) (s : Finset α) :
    Finset.map g (Finset.map f s) = Finset.map (f.trans g) s
    theorem Finset.map_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {β' : Type u_4} {f : β γ} {g : α β} {f' : α β'} {g' : β' γ} (h_comm : ∀ (a : α), f (g a) = g' (f' a)) :
    theorem Function.Semiconj.finset_map {α : Type u_1} {β : Type u_2} {f : α β} {ga : α α} {gb : β β} (h : Function.Semiconj f ga gb) :
    theorem Function.Commute.finset_map {α : Type u_1} {f : α α} {g : α α} (h : Function.Commute f g) :
    @[simp]
    theorem Finset.map_subset_map {α : Type u_1} {β : Type u_2} {f : α β} {s₁ : Finset α} {s₂ : Finset α} :
    Finset.map f s₁ Finset.map f s₂ s₁ s₂
    theorem GCongr.finsetMap_subset {α : Type u_1} {β : Type u_2} {f : α β} {s₁ : Finset α} {s₂ : Finset α} :
    s₁ s₂Finset.map f s₁ Finset.map f s₂

    Alias of the reverse direction of Finset.map_subset_map.

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

    The Finset version of Equiv.subset_symm_image.

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

    The Finset version of Equiv.symm_image_subset.

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

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

    Equations
    Instances For
      @[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 : α β) :
      @[simp]
      theorem Finset.map_ssubset_map {α : Type u_1} {β : Type u_2} {f : α β} {s : Finset α} {t : Finset α} :
      theorem GCongr.finsetMap_ssubset {α : Type u_1} {β : Type u_2} {f : α β} {s : Finset α} {t : Finset α} :
      s tFinset.map f s Finset.map f t

      Alias of the reverse direction of Finset.map_ssubset_map.

      @[simp]
      theorem Finset.mapEmbedding_apply {α : Type u_1} {β : Type u_2} {f : α β} {s : Finset α} :
      theorem Finset.filter_map {α : Type u_1} {β : Type u_2} {f : α β} {s : Finset α} {p : βProp} [DecidablePred p] :
      theorem Finset.map_filter' {α : Type u_1} {β : Type u_2} (p : αProp) [DecidablePred p] (f : α β) (s : Finset α) [DecidablePred fun (x : β) => ∃ (a : α), p a f a = x] :
      Finset.map f (Finset.filter p s) = Finset.filter (fun (b : β) => ∃ (a : α), p a f a = b) (Finset.map f s)
      theorem Finset.filter_attach' {α : Type u_1} [DecidableEq α] (s : Finset α) (p : { x : α // x s }Prop) [DecidablePred p] :
      Finset.filter p s.attach = Finset.map { toFun := Subtype.map id , inj' := } (Finset.filter (fun (x : α) => ∃ (h : x s), p x, h) s).attach
      theorem Finset.filter_attach {α : Type u_1} (p : αProp) [DecidablePred p] (s : Finset α) :
      Finset.filter (fun (a : { x : α // x s }) => p a) s.attach = Finset.map ((Function.Embedding.refl α).subtypeMap ) (Finset.filter p s).attach
      theorem Finset.map_filter {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α β} {p : αProp} [DecidablePred p] :
      Finset.map f.toEmbedding (Finset.filter p s) = Finset.filter (p f.symm) (Finset.map f.toEmbedding s)
      @[simp]
      theorem Finset.disjoint_map {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset α} (f : α β) :
      theorem Finset.map_disjUnion {α : Type u_1} {β : Type u_2} {f : α β} (s₁ : Finset α) (s₂ : Finset α) (h : Disjoint s₁ s₂) (h' : optParam (Disjoint (Finset.map f s₁) (Finset.map f s₂)) ) :
      Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'
      theorem Finset.map_disjUnion' {α : Type u_1} {β : Type u_2} {f : α β} (s₁ : Finset α) (s₂ : Finset α) (h' : Disjoint (Finset.map f s₁) (Finset.map f s₂)) (h : optParam (Disjoint s₁ s₂) ) :
      Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'

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

      theorem Finset.map_union {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α β} (s₁ : Finset α) (s₂ : Finset α) :
      Finset.map f (s₁ s₂) = Finset.map f s₁ Finset.map f s₂
      theorem Finset.map_inter {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α β} (s₁ : Finset α) (s₂ : Finset α) :
      Finset.map f (s₁ s₂) = Finset.map f s₁ Finset.map f s₂
      @[simp]
      theorem Finset.map_singleton {α : Type u_1} {β : Type u_2} (f : α β) (a : α) :
      Finset.map f {a} = {f a}
      @[simp]
      theorem Finset.map_insert {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α β) (a : α) (s : Finset α) :
      Finset.map f (insert a s) = insert (f a) (Finset.map f s)
      @[simp]
      theorem Finset.map_cons {α : Type u_1} {β : Type u_2} (f : α β) (a : α) (s : Finset α) (ha : as) :
      Finset.map f (Finset.cons a s ha) = Finset.cons (f a) (Finset.map f s)
      @[simp]
      theorem Finset.map_eq_empty {α : Type u_1} {β : Type u_2} {f : α β} {s : Finset α} :
      @[simp]
      theorem Finset.map_nonempty {α : Type u_1} {β : Type u_2} {f : α β} {s : Finset α} :
      (Finset.map f s).Nonempty s.Nonempty
      theorem Finset.Nonempty.map {α : Type u_1} {β : Type u_2} {f : α β} {s : Finset α} :
      s.Nonempty(Finset.map f s).Nonempty

      Alias of the reverse direction of Finset.map_nonempty.

      @[simp]
      theorem Finset.map_nontrivial {α : Type u_1} {β : Type u_2} {f : α β} {s : Finset α} :
      (Finset.map f s).Nontrivial s.Nontrivial
      theorem Finset.attach_map_val {α : Type u_1} {s : Finset α} :
      Finset.map (Function.Embedding.subtype fun (x : α) => x s) s.attach = s
      theorem Finset.map_disjiUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {s : Finset α} {t : βFinset γ} {h : (↑(Finset.map f s)).PairwiseDisjoint t} :
      (Finset.map f s).disjiUnion t h = s.disjiUnion (fun (a : α) => t (f a))
      theorem Finset.disjiUnion_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : αFinset β} {f : β γ} {h : (↑s).PairwiseDisjoint t} :
      Finset.map f (s.disjiUnion t h) = s.disjiUnion (fun (a : α) => Finset.map f (t a))
      theorem Finset.range_add_one' (n : ) :
      Finset.range (n + 1) = insert 0 (Finset.map { toFun := fun (i : ) => i + 1, inj' := } (Finset.range n))

      image #

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

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

      Equations
      Instances For
        @[simp]
        theorem Finset.image_val {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : αβ) (s : Finset α) :
        (Finset.image f s).val = (Multiset.map f s.val).dedup
        @[simp]
        theorem Finset.image_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : αβ) :
        @[simp]
        theorem Finset.mem_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} {b : β} :
        b Finset.image f s as, f a = b
        theorem Finset.mem_image_of_mem {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (f : αβ) {a : α} (h : a s) :
        theorem Finset.forall_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} {p : βProp} :
        (∀ bFinset.image f s, p b) as, p (f a)
        theorem Finset.map_eq_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α β) (s : Finset α) :
        theorem Finset.mem_image_const {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {b : β} {c : β} :
        c Finset.image (Function.const α b) s s.Nonempty b = c
        theorem Finset.mem_image_const_self {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {b : β} :
        b Finset.image (Function.const α b) s s.Nonempty
        instance Finset.canLift {α : Type u_1} {β : Type u_2} [DecidableEq β] (c : αβ) (p : βProp) [CanLift β α c p] :
        CanLift (Finset β) (Finset α) (Finset.image c) fun (s : Finset β) => xs, p x
        Equations
        • =
        theorem Finset.image_congr {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {g : αβ} {s : Finset α} (h : Set.EqOn f g s) :
        theorem Function.Injective.mem_finset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} {a : α} (hf : Function.Injective f) :
        f a Finset.image f s a s
        @[simp]
        theorem Finset.coe_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} :
        (Finset.image f s) = f '' s
        @[simp]
        theorem Finset.image_nonempty {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} :
        (Finset.image f s).Nonempty s.Nonempty
        theorem Finset.Nonempty.image {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (h : s.Nonempty) (f : αβ) :
        (Finset.image f s).Nonempty
        theorem Finset.Nonempty.of_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} :
        (Finset.image f s).Nonemptys.Nonempty

        Alias of the forward direction of Finset.image_nonempty.

        @[deprecated Finset.image_nonempty]
        theorem Finset.Nonempty.image_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (f : αβ) :
        (Finset.image f s).Nonempty s.Nonempty
        theorem Finset.image_toFinset {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} [DecidableEq α] {s : Multiset α} :
        Finset.image f s.toFinset = (Multiset.map f s).toFinset
        theorem Finset.image_val_of_injOn {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} (H : Set.InjOn f s) :
        (Finset.image f s).val = Multiset.map f s.val
        @[simp]
        theorem Finset.image_id {α : Type u_1} {s : Finset α} [DecidableEq α] :
        @[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 : βγ} :
        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)) :
        theorem Function.Semiconj.finset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : αβ} {ga : αα} {gb : ββ} (h : Function.Semiconj f ga gb) :
        theorem Function.Commute.finset_image {α : Type u_1} [DecidableEq α] {f : αα} {g : αα} (h : Function.Commute f g) :
        theorem Finset.image_subset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s₁ : Finset α} {s₂ : Finset α} (h : s₁ s₂) :
        theorem Finset.image_subset_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} {t : Finset β} :
        Finset.image f s t xs, f x t
        theorem Finset.image_mono {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : αβ) :
        theorem Finset.image_injective {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} (hf : Function.Injective f) :
        theorem Finset.image_inj {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} {t : Finset α} (hf : Function.Injective f) :
        theorem Finset.image_subset_image_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} {t : Finset α} (hf : Function.Injective f) :
        theorem Finset.image_ssubset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} {t : Finset α} (hf : Function.Injective f) :
        theorem Finset.coe_image_subset_range {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} :
        theorem Finset.filter_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} {p : βProp} [DecidablePred p] :
        Finset.filter p (Finset.image f s) = Finset.image f (Finset.filter (fun (a : α) => p (f a)) s)
        @[deprecated Finset.filter_mem_eq_inter]
        theorem Finset.filter_mem_image_eq_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : αβ) (s : Finset α) (t : Finset β) (h : xs, f x t) :
        Finset.filter (fun (y : β) => y Finset.image f s) t = Finset.image f s
        theorem Finset.fiber_nonempty_iff_mem_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} {y : β} :
        (Finset.filter (fun (x : α) => f x = y) s).Nonempty y Finset.image f s
        theorem Finset.image_union {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : αβ} (s₁ : Finset α) (s₂ : Finset α) :
        Finset.image f (s₁ s₂) = Finset.image f s₁ Finset.image f s₂
        theorem Finset.image_inter_subset {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : αβ) (s : Finset α) (t : Finset α) :
        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)) :
        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 α) :
        theorem Finset.erase_image_subset_image_erase {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : αβ) (s : Finset α) (a : α) :
        (Finset.image f s).erase (f a) Finset.image f (s.erase a)
        @[simp]
        theorem Finset.image_erase {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : αβ} (hf : Function.Injective f) (s : Finset α) (a : α) :
        Finset.image f (s.erase a) = (Finset.image f s).erase (f a)
        @[simp]
        theorem Finset.image_eq_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : αβ} {s : Finset α} :
        theorem Finset.image_sdiff {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : αβ} (s : Finset α) (t : Finset α) (hf : Function.Injective f) :
        theorem Finset.image_symmDiff {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {f : αβ} (s : Finset α) (t : Finset α) (hf : Function.Injective f) :
        @[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)) :
        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)
        @[simp]
        theorem Finset.attach_image_val {α : Type u_1} [DecidableEq α] {s : Finset α} :
        Finset.image Subtype.val s.attach = s
        @[simp]
        theorem Finset.attach_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} :
        (insert a s).attach = insert a, (Finset.image (fun (x : { x : α // x s }) => x, ) s.attach)
        @[simp]
        theorem Finset.disjoint_image {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : Finset α} {f : αβ} (hf : Function.Injective f) :
        theorem Finset.image_const {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (h : s.Nonempty) (b : β) :
        Finset.image (fun (x : α) => b) s = {b}
        @[simp]
        theorem Finset.map_erase {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : α β) (s : Finset α) (a : α) :
        Finset.map f (s.erase a) = (Finset.map f s).erase (f a)
        theorem Finset.image_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {f : αβ} {s : Finset α} {t : βFinset γ} :
        (Finset.image f s).biUnion t = s.biUnion fun (a : α) => t (f a)
        theorem Finset.biUnion_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {s : Finset α} {t : αFinset β} {f : βγ} :
        Finset.image f (s.biUnion t) = s.biUnion fun (a : α) => Finset.image f (t a)
        theorem Finset.image_biUnion_filter_eq {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (s : Finset β) (g : βα) :
        ((Finset.image g s).biUnion fun (a : α) => Finset.filter (fun (c : β) => g c = a) s) = s
        theorem Finset.biUnion_singleton {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {f : αβ} :
        (s.biUnion fun (a : α) => {f a}) = Finset.image f s

        filterMap #

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

        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
        Instances For
          @[simp]
          theorem Finset.filterMap_val {α : Type u_1} {β : Type u_2} (f : αOption β) (s' : Finset α) {f_inj : ∀ (a a' : α), bf a, b f a'a = a'} :
          (Finset.filterMap f s' f_inj).val = Multiset.filterMap f s'.val
          @[simp]
          theorem Finset.filterMap_empty {α : Type u_1} {β : Type u_2} (f : αOption β) {f_inj : ∀ (a a' : α), bf a, b f a'a = a'} :
          @[simp]
          theorem Finset.mem_filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) {s : Finset α} {f_inj : ∀ (a a' : α), bf a, b f a'a = a'} {b : β} :
          b Finset.filterMap f s f_inj as, f a = some b
          @[simp]
          theorem Finset.coe_filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) {s : Finset α} {f_inj : ∀ (a a' : α), bf a, b f a'a = a'} :
          (Finset.filterMap f s f_inj) = {b : β | as, f a = some b}
          @[simp]
          theorem Finset.filterMap_some {α : Type u_1} {s : Finset α} :
          Finset.filterMap some s = s
          theorem Finset.filterMap_mono {α : Type u_1} {β : Type u_2} (f : αOption β) {s : Finset α} {t : Finset α} {f_inj : ∀ (a a' : α), bf a, b f a'a = a'} (h : s t) :

          Subtype #

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

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

          Equations
          Instances For
            @[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 xxs
            theorem Finset.subtype_mono {α : Type u_1} {p : αProp} [DecidablePred p] :
            @[simp]

            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 : xs, p x) :

            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) :
            aFinset.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 ) :

            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
            Instances For
              @[simp]
              theorem Finset.mem_fin {n : } {s : Finset } (a : Fin n) :
              a Finset.fin n s a s
              @[simp]
              theorem Finset.fin_map {n : } {s : Finset } :
              Finset.map Fin.valEmbedding (Finset.fin n s) = Finset.filter (fun (x : ) => x < n) s
              theorem Finset.subset_image_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : Finset β} {f : αβ} :
              t Finset.image f s s's, Finset.image f s' = t

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

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

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

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

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

              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
                @[simp]
                theorem Equiv.finsetCongr_apply {α : Type u_1} {β : Type u_2} (e : α β) (s : Finset α) :
                e.finsetCongr s = Finset.map e.toEmbedding s
                @[simp]
                theorem Equiv.finsetCongr_refl {α : Type u_1} :
                (Equiv.refl α).finsetCongr = Equiv.refl (Finset α)
                @[simp]
                theorem Equiv.finsetCongr_symm {α : Type u_1} {β : Type u_2} (e : α β) :
                e.finsetCongr.symm = e.symm.finsetCongr
                @[simp]
                theorem Equiv.finsetCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (e' : β γ) :
                e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr
                theorem Equiv.finsetCongr_toEmbedding {α : Type u_1} {β : Type u_2} (e : α β) :
                e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding