Mathlib.Data.Finset.Image

Finset.map definition

(f : α ↪ β) (s : Finset α) : Finset β

Full source

/-- 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. -/
def map (f : α ↪ β) (s : Finset α) : Finset β :=
  ⟨s.1.map f, s.2.map f.2⟩

Image of a finite set under an injective embedding

Informal description

Given an injective function embedding $ f : \alpha \hookrightarrow \beta $ and a finite set $ s $ in $ \alpha $, the operation $ \text{map} $ constructs the image finite set in $ \beta $ by applying $ f $ to each element of $ s $. The injectivity of $ f $ ensures there are no duplicate elements in the resulting finite set.

Finset.map_val theorem

(f : α ↪ β) (s : Finset α) : (map f s).1 = s.1.map f

Full source

@[simp]
theorem map_val (f : α ↪ β) (s : Finset α) : (map f s).1 = s.1.map f :=
  rfl

Multiset Equality for Image of Finite Set under Injective Embedding

Informal description

For any injective function embedding $f : \alpha \hookrightarrow \beta$ and finite set $s \subseteq \alpha$, the underlying multiset of the image set $\text{map}(f)(s)$ is equal to the image of the underlying multiset of $s$ under $f$. In other words, the multiset equality $( \text{map}(f)(s) ).1 = s.1.\text{map}(f)$ holds.

Finset.map_empty theorem

(f : α ↪ β) : (∅ : Finset α).map f = ∅

Full source

@[simp]
theorem map_empty (f : α ↪ β) : (∅ : Finset α).map f = ∅ :=
  rfl

Image of Empty Set under Injective Embedding is Empty

Informal description

For any injective function embedding $f : \alpha \hookrightarrow \beta$, the image of the empty finite set under $f$ is the empty set, i.e., $\text{map}(f)(\emptyset) = \emptyset$.

Finset.mem_map theorem

{b : β} : b ∈ s.map f ↔ ∃ a ∈ s, f a = b

Full source

@[simp]
theorem mem_map {b : β} : b ∈ s.map fb ∈ s.map f ↔ ∃ a ∈ s, f a = b :=
  Multiset.mem_map

Characterization of Membership in Image of Finite Set under Injective Embedding

Informal description

For any element $b \in \beta$ and finite set $s \subseteq \alpha$, $b$ belongs to the image of $s$ under the injective embedding $f : \alpha \hookrightarrow \beta$ if and only if there exists an element $a \in s$ such that $f(a) = b$. In other words: $$ b \in \text{map}(f)(s) \leftrightarrow \exists a \in s, f(a) = b $$

Finset.mem_map_equiv theorem

{f : α ≃ β} {b : β} : b ∈ s.map f.toEmbedding ↔ f.symm b ∈ s

Full source

@[simp 1100]
theorem mem_map_equiv {f : α ≃ β} {b : β} : b ∈ s.map f.toEmbeddingb ∈ s.map f.toEmbedding ↔ f.symm b ∈ s := by
  rw [mem_map]
  exact
    ⟨by
      rintro ⟨a, H, rfl⟩
      simpa, fun h => ⟨_, h, by simp⟩⟩

Characterization of Membership in Image via Equivalence: $b \in \text{map}(f)(s) \leftrightarrow f^{-1}(b) \in s$

Informal description

For any equivalence (bijection) $f : \alpha \simeq \beta$, an element $b \in \beta$, and a finite set $s \subseteq \alpha$, the element $b$ belongs to the image of $s$ under the injective embedding $f$ if and only if the inverse image $f^{-1}(b)$ belongs to $s$. In other words: $$ b \in \text{map}(f)(s) \leftrightarrow f^{-1}(b) \in s $$

Finset.mem_map' theorem

(f : α ↪ β) {a} {s : Finset α} : f a ∈ s.map f ↔ a ∈ s

Full source

@[simp 1100]
theorem mem_map' (f : α ↪ β) {a} {s : Finset α} : f a ∈ s.map ff a ∈ s.map f ↔ a ∈ s :=
  mem_map_of_injective f.2

Membership in Image of Finite Set under Injective Embedding

Informal description

For an injective function embedding $f : \alpha \hookrightarrow \beta$, an element $a \in \alpha$, and a finite set $s \subseteq \alpha$, the image $f(a)$ belongs to the image set $s.map(f)$ if and only if $a$ belongs to $s$. In other words, $f(a) \in s.map(f) \leftrightarrow a \in s$.

Finset.mem_map_of_mem theorem

(f : α ↪ β) {a} {s : Finset α} : a ∈ s → f a ∈ s.map f

Full source

theorem mem_map_of_mem (f : α ↪ β) {a} {s : Finset α} : a ∈ s → f a ∈ s.map f :=
  (mem_map' _).2

Image of Element under Injective Embedding Preserves Membership in Finite Sets

Informal description

For any injective function embedding $f : \alpha \hookrightarrow \beta$, an element $a \in \alpha$, and a finite set $s \subseteq \alpha$, if $a$ belongs to $s$, then its image $f(a)$ belongs to the image set $s.map(f)$.

Finset.forall_mem_map theorem

 {f : α ↪ β} {s : Finset α} {p : ∀ a, a ∈ s.map f → Prop} :
  (∀ y (H : y ∈ s.map f), p y H) ↔ ∀ x (H : x ∈ s), p (f x) (mem_map_of_mem _ H)

Full source

theorem forall_mem_map {f : α ↪ β} {s : Finset α} {p : ∀ a, a ∈ s.map f → Prop} :
    (∀ y (H : y ∈ s.map f), p y H) ↔ ∀ x (H : x ∈ s), p (f x) (mem_map_of_mem _ H) :=
  ⟨fun h y hy => h (f y) (mem_map_of_mem _ hy),
   fun h x hx => by
    obtain ⟨y, hy, rfl⟩ := mem_map.1 hx
    exact h _ hy⟩

Universal Property of Image under Injective Map for Finite Sets

Informal description

Let $f : \alpha \hookrightarrow \beta$ be an injective function, $s$ be a finite subset of $\alpha$, and $p$ be a predicate on elements of $\beta$ that depends on their membership in $s.map(f)$. Then the following are equivalent: 1. For every $y \in s.map(f)$, the predicate $p(y)$ holds. 2. For every $x \in s$, the predicate $p(f(x))$ holds. In other words, a property holds for all elements in the image of $s$ under $f$ if and only if it holds for all images of elements in $s$ under $f$.

Finset.apply_coe_mem_map theorem

(f : α ↪ β) (s : Finset α) (x : s) : f x ∈ s.map f

Full source

theorem apply_coe_mem_map (f : α ↪ β) (s : Finset α) (x : s) : f x ∈ s.map f :=
  mem_map_of_mem f x.prop

Membership Preservation under Injective Map for Finite Sets

Informal description

Let $f : \alpha \hookrightarrow \beta$ be an injective function, $s$ be a finite subset of $\alpha$, and $x$ be an element of $s$ (viewed as a term of the subtype $\{a \in \alpha \mid a \in s\}$). Then the image $f(x)$ belongs to the image set $s.map(f)$.

Finset.coe_map theorem

(f : α ↪ β) (s : Finset α) : (s.map f : Set β) = f '' s

Full source

@[simp, norm_cast]
theorem coe_map (f : α ↪ β) (s : Finset α) : (s.map f : Set β) = f '' s :=
  Set.ext (by simp only [mem_coe, mem_map, Set.mem_image, implies_true])

Equality of Set Images under Injective Map for Finite Sets

Informal description

Let $f : \alpha \hookrightarrow \beta$ be an injective function and $s$ be a finite subset of $\alpha$. Then the underlying set of the image of $s$ under $f$ (via `Finset.map`) is equal to the image of $s$ under $f$ as sets, i.e., $\{f(x) \mid x \in s\} = f(s)$ as subsets of $\beta$.

Finset.coe_map_subset_range theorem

(f : α ↪ β) (s : Finset α) : (s.map f : Set β) ⊆ Set.range f

Full source

theorem coe_map_subset_range (f : α ↪ β) (s : Finset α) : (s.map f : Set β) ⊆ Set.range f :=
  calc
    ↑(s.map f) = f '' s := coe_map f s
    _ ⊆ Set.range f := Set.image_subset_range f ↑s

Image of Finite Set under Injective Map is Subset of Range

Informal description

For any injective function $f : \alpha \hookrightarrow \beta$ and any finite subset $s \subseteq \alpha$, the image of $s$ under $f$ (as a set) is a subset of the range of $f$, i.e., $f(s) \subseteq \text{range}(f)$.

Finset.map_perm theorem

{σ : Equiv.Perm α} (hs : {a | σ a ≠ a} ⊆ s) : s.map (σ : α ↪ α) = s

Full source

/-- If the only elements outside `s` are those left fixed by `σ`, then mapping by `σ` has no effect.
-/
theorem map_perm {σ : Equiv.Perm α} (hs : { a | σ a ≠ a }{ a | σ a ≠ a } ⊆ s) : s.map (σ : α ↪ α) = s :=
  coe_injective <| (coe_map _ _).trans <| Set.image_perm hs

Invariance of Finite Set under Permutation: $\sigma(s) = s$ when $\sigma$ moves only elements in $s$

Informal description

Let $s$ be a finite subset of a type $\alpha$ and $\sigma : \alpha \to \alpha$ be a permutation of $\alpha$. If the set of elements not fixed by $\sigma$ is contained in $s$ (i.e., $\{a \in \alpha \mid \sigma(a) \neq a\} \subseteq s$), then the image of $s$ under $\sigma$ is equal to $s$ itself, i.e., $s.\mathrm{map}(\sigma) = s$.

Finset.map_toFinset theorem

[DecidableEq α] [DecidableEq β] {s : Multiset α} : s.toFinset.map f = (s.map f).toFinset

Full source

theorem map_toFinset [DecidableEq α] [DecidableEq β] {s : Multiset α} :
    s.toFinset.map f = (s.map f).toFinset :=
  ext fun _ => by simp only [mem_map, Multiset.mem_map, exists_prop, Multiset.mem_toFinset]

Commutativity of Map and Finite Set Construction for Multisets

Informal description

For any multiset $s$ of elements of type $\alpha$ with decidable equality on both $\alpha$ and $\beta$, the image of the finite set constructed from $s$ under an injective embedding $f : \alpha \hookrightarrow \beta$ is equal to the finite set constructed from the multiset image of $s$ under $f$. In other words, $(s.\text{toFinset}).\text{map} f = (s.\text{map} f).\text{toFinset}$.

Finset.map_refl theorem

: s.map (Embedding.refl _) = s

Full source

@[simp]
theorem map_refl : s.map (Embedding.refl _) = s :=
  ext fun _ => by simpa only [mem_map, exists_prop] using exists_eq_right

Image of Finite Set under Identity Embedding is Itself

Informal description

For any finite set $s$ of type $\alpha$, the image of $s$ under the identity embedding $\mathrm{id} : \alpha \hookrightarrow \alpha$ is equal to $s$ itself. That is, $s.\mathrm{map}(\mathrm{id}) = s$.

Finset.map_cast_heq theorem

{α β} (h : α = β) (s : Finset α) : HEq (s.map (Equiv.cast h).toEmbedding) s

Full source

@[simp]
theorem map_cast_heq {α β} (h : α = β) (s : Finset α) :
    HEq (s.map (Equiv.cast h).toEmbedding) s := by
  subst h
  simp

Hereditary Equality of Finite Set Image under Type Casting Embedding

Informal description

Given two types $\alpha$ and $\beta$ with a proof $h$ that $\alpha = \beta$, and a finite set $s$ of elements of type $\alpha$, the image of $s$ under the embedding induced by the type casting equivalence $\mathrm{Equiv.cast}\,h$ is hereditarily equal to $s$ itself.

Finset.map_map theorem

(f : α ↪ β) (g : β ↪ γ) (s : Finset α) : (s.map f).map g = s.map (f.trans g)

Full source

theorem map_map (f : α ↪ β) (g : β ↪ γ) (s : Finset α) : (s.map f).map g = s.map (f.trans g) :=
  eq_of_veq <| by simp only [map_val, Multiset.map_map]; rfl

Composition of Images under Injective Embeddings for Finite Sets

Informal description

Let $f : \alpha \hookrightarrow \beta$ and $g : \beta \hookrightarrow \gamma$ be injective function embeddings, and let $s$ be a finite subset of $\alpha$. Then the image of $s$ under $f$ followed by the image under $g$ is equal to the image of $s$ under the composition $g \circ f$ of the embeddings.

Finset.map_comm theorem

 {β'} {f : β ↪ γ} {g : α ↪ β} {f' : α ↪ β'} {g' : β' ↪ γ} (h_comm : ∀ a, f (g a) = g' (f' a)) :
  (s.map g).map f = (s.map f').map g'

Full source

theorem map_comm {β'} {f : β ↪ γ} {g : α ↪ β} {f' : α ↪ β'} {g' : β' ↪ γ}
    (h_comm : ∀ a, f (g a) = g' (f' a)) : (s.map g).map f = (s.map f').map g' := by
  simp_rw [map_map, Embedding.trans, Function.comp_def, h_comm]

Commutativity of Image Operations under Injective Embeddings for Finite Sets

Informal description

Let $f : \beta \hookrightarrow \gamma$ and $g : \alpha \hookrightarrow \beta$ be injective embeddings, and let $f' : \alpha \hookrightarrow \beta'$ and $g' : \beta' \hookrightarrow \gamma$ be another pair of injective embeddings. If for all $a \in \alpha$ we have the commutative relation $f(g(a)) = g'(f'(a))$, then for any finite set $s \subseteq \alpha$, the image of $s$ under $g$ followed by $f$ equals the image of $s$ under $f'$ followed by $g'$. That is, $(s \map g) \map f = (s \map f') \map g'$.

Function.Semiconj.finset_map theorem

 {f : α ↪ β} {ga : α ↪ α} {gb : β ↪ β} (h : Function.Semiconj f ga gb) : Function.Semiconj (map f) (map ga) (map gb)

Full source

theorem _root_.Function.Semiconj.finset_map {f : α ↪ β} {ga : α ↪ α} {gb : β ↪ β}
    (h : Function.Semiconj f ga gb) : Function.Semiconj (map f) (map ga) (map gb) := fun _ =>
  map_comm h

Semiconjugacy of Finite Set Images under Injective Embeddings

Informal description

Let $f : \alpha \hookrightarrow \beta$ be an injective function embedding, and let $g_a : \alpha \hookrightarrow \alpha$ and $g_b : \beta \hookrightarrow \beta$ be injective embeddings such that $f$ semiconjugates $g_a$ and $g_b$, i.e., $f \circ g_a = g_b \circ f$. Then for any finite set $s \subseteq \alpha$, the image of $s$ under $g_a$ followed by $f$ equals the image of $s$ under $f$ followed by $g_b$. That is, $f(g_a(s)) = g_b(f(s))$.

Function.Commute.finset_map theorem

{f g : α ↪ α} (h : Function.Commute f g) : Function.Commute (map f) (map g)

Full source

theorem _root_.Function.Commute.finset_map {f g : α ↪ α} (h : Function.Commute f g) :
    Function.Commute (map f) (map g) :=
  Function.Semiconj.finset_map h

Commutation of Image Operations for Commuting Injective Embeddings on Finite Sets

Informal description

Let $f, g : \alpha \hookrightarrow \alpha$ be commuting injective embeddings, i.e., $f \circ g = g \circ f$. Then for any finite set $s \subseteq \alpha$, the image operations on finite sets also commute: $f(g(s)) = g(f(s))$.

Finset.map_subset_map theorem

{s₁ s₂ : Finset α} : s₁.map f ⊆ s₂.map f ↔ s₁ ⊆ s₂

Full source

@[simp]
theorem map_subset_map {s₁ s₂ : Finset α} : s₁.map f ⊆ s₂.map fs₁.map f ⊆ s₂.map f ↔ s₁ ⊆ s₂ :=
  ⟨fun h _ xs => (mem_map' _).1 <| h <| (mem_map' f).2 xs,
   fun h => by simp [subset_def, Multiset.map_subset_map h]⟩

Image Subset Relation under Injective Embedding: $f(s_1) \subseteq f(s_2) \leftrightarrow s_1 \subseteq s_2$

Informal description

For any two finite subsets $s_1$ and $s_2$ of a type $\alpha$, and an injective function embedding $f : \alpha \hookrightarrow \beta$, the image of $s_1$ under $f$ is a subset of the image of $s_2$ under $f$ if and only if $s_1$ is a subset of $s_2$. In other words: $$ f(s_1) \subseteq f(s_2) \leftrightarrow s_1 \subseteq s_2. $$

Finset.subset_map_symm theorem

{t : Finset β} {f : α ≃ β} : s ⊆ t.map f.symm ↔ s.map f ⊆ t

Full source

/-- The `Finset` version of `Equiv.subset_symm_image`. -/
theorem subset_map_symm {t : Finset β} {f : α ≃ β} : s ⊆ t.map f.symms ⊆ t.map f.symm ↔ s.map f ⊆ t := by
  constructor <;> intro h x hx
  · simp only [mem_map_equiv, Equiv.symm_symm] at hx
    simpa using h hx
  · simp only [mem_map_equiv]
    exact h (by simp [hx])

Subset Relation under Equivalence and its Inverse

Informal description

For any finite set $s$ in $\alpha$, any finite set $t$ in $\beta$, and any equivalence $f : \alpha \simeq \beta$, the following holds: $$ s \subseteq f^{-1}(t) \leftrightarrow f(s) \subseteq t. $$

Finset.map_symm_subset theorem

{t : Finset β} {f : α ≃ β} : t.map f.symm ⊆ s ↔ t ⊆ s.map f

Full source

/-- The `Finset` version of `Equiv.symm_image_subset`. -/
theorem map_symm_subset {t : Finset β} {f : α ≃ β} : t.map f.symm ⊆ st.map f.symm ⊆ s ↔ t ⊆ s.map f := by
  simp only [← subset_map_symm, Equiv.symm_symm]

Subset Relation under Equivalence and its Inverse

Informal description

For any finite set $t$ in $\beta$ and any equivalence $f : \alpha \simeq \beta$, the image of $t$ under the inverse equivalence $f^{-1}$ is a subset of $s$ if and only if $t$ is a subset of the image of $s$ under $f$. In other words: $$ f^{-1}(t) \subseteq s \leftrightarrow t \subseteq f(s). $$

Finset.mapEmbedding definition

(f : α ↪ β) : Finset α ↪o Finset β

Full source

/-- Associate to an embedding `f` from `α` to `β` the order embedding that maps a finset to its
image under `f`. -/
def mapEmbedding (f : α ↪ β) : FinsetFinset α ↪o Finset β :=
  OrderEmbedding.ofMapLEIff (map f) fun _ _ => map_subset_map

Order embedding of finite sets under injective map

Informal description

Given an injective function embedding $ f : \alpha \hookrightarrow \beta $, the operation `mapEmbedding` constructs an order embedding from the finite subsets of $\alpha$ to the finite subsets of $\beta$, where the order relation is preserved and reflected. Specifically, for any two finite subsets $ s_1 $ and $ s_2 $ of $\alpha$, we have $ s_1 \subseteq s_2 $ if and only if $ f(s_1) \subseteq f(s_2) $.

Finset.map_inj theorem

{s₁ s₂ : Finset α} : s₁.map f = s₂.map f ↔ s₁ = s₂

Full source

@[simp]
theorem map_inj {s₁ s₂ : Finset α} : s₁.map f = s₂.map f ↔ s₁ = s₂ :=
  (mapEmbedding f).injective.eq_iff

Injectivity of Finite Set Image under Injective Map

Informal description

For any two finite subsets $s_1$ and $s_2$ of a type $\alpha$, and any injective function embedding $f : \alpha \hookrightarrow \beta$, the images of $s_1$ and $s_2$ under $f$ are equal if and only if $s_1$ and $s_2$ are equal. In other words: $$ f(s_1) = f(s_2) \leftrightarrow s_1 = s_2. $$

Finset.map_injective theorem

(f : α ↪ β) : Injective (map f)

Full source

theorem map_injective (f : α ↪ β) : Injective (map f) :=
  (mapEmbedding f).injective

Injectivity of Finite Set Mapping under Injective Embedding

Informal description

For any injective function embedding $f : \alpha \hookrightarrow \beta$, the map operation on finite sets $s \mapsto s.\text{map}(f)$ is injective. That is, for any two finite subsets $s_1, s_2$ of $\alpha$, if $s_1.\text{map}(f) = s_2.\text{map}(f)$, then $s_1 = s_2$.

Finset.map_ssubset_map theorem

{s t : Finset α} : s.map f ⊂ t.map f ↔ s ⊂ t

Full source

@[simp]
theorem map_ssubset_map {s t : Finset α} : s.map f ⊂ t.map fs.map f ⊂ t.map f ↔ s ⊂ t := (mapEmbedding f).lt_iff_lt

Strict Subset Preservation under Injective Map

Informal description

For any finite subsets $s$ and $t$ of $\alpha$, the image of $s$ under the injective embedding $f$ is a strict subset of the image of $t$ under $f$ if and only if $s$ is a strict subset of $t$. In other words, $$ f(s) \subset f(t) \leftrightarrow s \subset t. $$

Finset.mapEmbedding_apply theorem

: mapEmbedding f s = map f s

Full source

@[simp]
theorem mapEmbedding_apply : mapEmbedding f s = map f s :=
  rfl

Image of Finite Set under Order Embedding Equals Map Image

Informal description

For any injective function embedding $f \colon \alpha \hookrightarrow \beta$ and any finite subset $s$ of $\alpha$, the image of $s$ under the order embedding $\text{mapEmbedding}\ f$ is equal to the image of $s$ under the map operation $\text{map}\ f$.

Finset.filter_map theorem

{p : β → Prop} [DecidablePred p] : (s.map f).filter p = (s.filter (p ∘ f)).map f

Full source

theorem filter_map {p : β → Prop} [DecidablePred p] :
    (s.map f).filter p = (s.filter (p ∘ f)).map f :=
  eq_of_veq (Multiset.filter_map _ _ _)

Filter-Map Commutation for Finite Sets: $\text{filter}\ p \circ \text{map}\ f = \text{map}\ f \circ \text{filter}\ (p \circ f)$

Informal description

Let $f : \alpha \hookrightarrow \beta$ be an injective function embedding, $s$ a finite subset of $\alpha$, and $p : \beta \to \text{Prop}$ a decidable predicate. Then filtering the image of $s$ under $f$ by $p$ is equivalent to first filtering $s$ by $p \circ f$ and then mapping the result under $f$. That is, \[ \text{filter}\ p\ (\text{map}\ f\ s) = \text{map}\ f\ (\text{filter}\ (p \circ f)\ s). \]

Finset.map_filter' theorem

 (p : α → Prop) [DecidablePred p] (f : α ↪ β) (s : Finset α) [DecidablePred (∃ a, p a ∧ f a = ·)] :
  (s.filter p).map f = (s.map f).filter fun b => ∃ a, p a ∧ f a = b

Full source

lemma map_filter' (p : α → Prop) [DecidablePred p] (f : α ↪ β) (s : Finset α)
    [DecidablePred (∃ a, p a ∧ f a = ·)] :
    (s.filter p).map f = (s.map f).filter fun b => ∃ a, p a ∧ f a = b := by
  simp [Function.comp_def, filter_map, f.injective.eq_iff]

Image-Filter Commutation for Finite Sets under Injective Embeddings

Informal description

Let $f \colon \alpha \hookrightarrow \beta$ be an injective function embedding, $s$ a finite subset of $\alpha$, and $p \colon \alpha \to \text{Prop}$ a decidable predicate. Suppose there is a decidable predicate on $\beta$ that checks whether an element $b$ satisfies $\exists a \in \alpha, p(a) \land f(a) = b$. Then the image under $f$ of the filtered subset $\{a \in s \mid p(a)\}$ is equal to the filtered subset of the image $\{f(a) \mid a \in s\}$ consisting of elements $b$ for which there exists $a \in s$ with $p(a)$ and $f(a) = b$. In symbols: \[ f\big(\{a \in s \mid p(a)\}\big) = \big\{b \in f(s) \mid \exists a \in s, p(a) \land f(a) = b\big\}. \]

Finset.filter_attach' theorem

 [DecidableEq α] (s : Finset α) (p : s → Prop) [DecidablePred p] :
  s.attach.filter p =
    (s.filter fun x => ∃ h, p ⟨x, h⟩).attach.map
      ⟨Subtype.map id <| filter_subset _ _, Subtype.map_injective _ injective_id⟩

Full source

lemma filter_attach' [DecidableEq α] (s : Finset α) (p : s → Prop) [DecidablePred p] :
    s.attach.filter p =
      (s.filter fun x => ∃ h, p ⟨x, h⟩).attach.map
        ⟨Subtype.map id <| filter_subset _ _, Subtype.map_injective _ injective_id⟩ :=
  eq_of_veq <| Multiset.filter_attach' _ _

Filter-Attach Commutation for Finite Sets: $\mathrm{filter}\, p \circ \mathrm{attach} = \mathrm{map}\, (\mathrm{id} \hookrightarrow \mathrm{mem\_of\_mem\_filter}) \circ \mathrm{attach} \circ \mathrm{filter}\, (\exists h, p \langle \cdot, h \rangle)$

Informal description

Let $s$ be a finite set of elements of type $\alpha$ with decidable equality, and let $p$ be a decidable predicate on the subtype $\{x \mid x \in s\}$. Then the filtered subset of the attached set $\{(x, h) \mid x \in s, h : x \in s\}$ under $p$ is equal to the attached set of the filtered subset $\{x \in s \mid \exists h, p \langle x, h \rangle\}$, mapped via the identity function on elements with proofs adjusted to show membership in the filtered set. In symbols: \[ \mathrm{filter}\, p\, (s.\mathrm{attach}) = \left(\mathrm{filter}\, (\lambda x, \exists h, p \langle x, h \rangle)\, s\right).\mathrm{attach}.\mathrm{map}\, \left(\mathrm{Subtype.map}\, \mathrm{id}\, (\lambda \_, \mathrm{mem\_of\_mem\_filter})\right) \]

Finset.filter_attach theorem

 (p : α → Prop) [DecidablePred p] (s : Finset α) :
  s.attach.filter (fun a : s ↦ p a) = (s.filter p).attach.map ((Embedding.refl _).subtypeMap mem_of_mem_filter)

Full source

lemma filter_attach (p : α → Prop) [DecidablePred p] (s : Finset α) :
    s.attach.filter (fun a : s ↦ p a) =
      (s.filter p).attach.map ((Embedding.refl _).subtypeMap mem_of_mem_filter) :=
  eq_of_veq <| Multiset.filter_attach _ _

Equality of Filtered Attached Finite Set and Mapped Attached Filtered Finite Set

Informal description

For any finite set $s$ of type $\alpha$ and a decidable predicate $p$ on $\alpha$, the filtered subset of the attached set $\{(a, h) \mid a \in s, h : a \in s\}$ under $p$ is equal to the attached set of the filtered subset $s.\mathrm{filter}\,p$, mapped via the identity embedding restricted to elements that satisfy the membership condition derived from the filter. More precisely, let $\mathrm{attach}(s) = \{(a, h) \mid a \in s, h : a \in s\}$ be the finite set of pairs where each element $a$ is paired with a proof $h$ of its membership in $s$. Then: \[ \mathrm{filter}\, p\, (\mathrm{attach}(s)) = \mathrm{map}\, (\mathrm{id}_{\,} \hookrightarrow \mathrm{mem\_of\_mem\_filter})\, (\mathrm{attach}(\mathrm{filter}\, p\, s)), \] where $\mathrm{id}_{\,} \hookrightarrow \mathrm{mem\_of\_mem\_filter}$ is the identity embedding restricted to elements that satisfy the membership condition derived from the filter.

Finset.map_filter theorem

 {f : α ≃ β} {p : α → Prop} [DecidablePred p] :
  (s.filter p).map f.toEmbedding = (s.map f.toEmbedding).filter (p ∘ f.symm)

Full source

theorem map_filter {f : α ≃ β} {p : α → Prop} [DecidablePred p] :
    (s.filter p).map f.toEmbedding = (s.map f.toEmbedding).filter (p ∘ f.symm) := by
  simp only [filter_map, Function.comp_def, Equiv.toEmbedding_apply, Equiv.symm_apply_apply]

Filter-Map Commutation under Equivalence: $\text{map}\ f \circ \text{filter}\ p = \text{filter}\ (p \circ f^{-1}) \circ \text{map}\ f$

Informal description

Let $f : \alpha \simeq \beta$ be an equivalence (bijection) between types $\alpha$ and $\beta$, $s$ a finite subset of $\alpha$, and $p : \alpha \to \text{Prop}$ a decidable predicate. Then the image under $f$ of the filtered subset $s \text{.filter } p$ is equal to the filtered image of $s$ under $f$ where the filter is composed with the inverse of $f$. That is, \[ \text{map } f \ (\text{filter } p \ s) = \text{filter } (p \circ f^{-1}) \ (\text{map } f \ s). \]

Finset.disjoint_map theorem

{s t : Finset α} (f : α ↪ β) : Disjoint (s.map f) (t.map f) ↔ Disjoint s t

Full source

@[simp]
theorem disjoint_map {s t : Finset α} (f : α ↪ β) :
    DisjointDisjoint (s.map f) (t.map f) ↔ Disjoint s t :=
  mod_cast Set.disjoint_image_iff f.injective (s := s) (t := t)

Disjointness of Images under Injective Embedding is Equivalent to Disjointness of Preimages

Informal description

For any finite sets $s, t \subseteq \alpha$ and an injective function embedding $f \colon \alpha \hookrightarrow \beta$, the images $f(s)$ and $f(t)$ are disjoint if and only if $s$ and $t$ are disjoint. In other words, $f(s) \cap f(t) = \emptyset \leftrightarrow s \cap t = \emptyset$.

Finset.map_union theorem

 [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) : (s₁ ∪ s₂).map f = s₁.map f ∪ s₂.map f

Full source

theorem map_union [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) :
    (s₁ ∪ s₂).map f = s₁.map f ∪ s₂.map f :=
  mod_cast Set.image_union f s₁ s₂

Image of Union under Injective Embedding: $f(s_1 \cup s_2) = f(s_1) \cup f(s_2)$

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality, and let $f : \alpha \hookrightarrow \beta$ be an injective function embedding. For any finite sets $s_1, s_2 \subseteq \alpha$, the image of their union under $f$ equals the union of their images under $f$, i.e., \[ f(s_1 \cup s_2) = f(s_1) \cup f(s_2). \]

Finset.map_inter theorem

 [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) : (s₁ ∩ s₂).map f = s₁.map f ∩ s₂.map f

Full source

theorem map_inter [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) :
    (s₁ ∩ s₂).map f = s₁.map f ∩ s₂.map f :=
  mod_cast Set.image_inter f.injective (s := s₁) (t := s₂)

Image of Intersection under Injective Embedding: $f(s_1 \cap s_2) = f(s_1) \cap f(s_2)$

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality, and let $f : \alpha \hookrightarrow \beta$ be an injective function embedding. For any finite sets $s_1, s_2 \subseteq \alpha$, the image of their intersection under $f$ equals the intersection of their images under $f$, i.e., \[ f(s_1 \cap s_2) = f(s_1) \cap f(s_2). \]

Finset.map_singleton theorem

(f : α ↪ β) (a : α) : map f { a } = {f a}

Full source

@[simp]
theorem map_singleton (f : α ↪ β) (a : α) : map f {a} = {f a} :=
  coe_injective <| by simp only [coe_map, coe_singleton, Set.image_singleton]

Image of Singleton Finite Set under Injective Map: $f(\{a\}) = \{f(a)\}$

Informal description

For any injective function $f \colon \alpha \hookrightarrow \beta$ and any element $a \in \alpha$, the image of the singleton finite set $\{a\}$ under $f$ is the singleton finite set $\{f(a)\}$.

Finset.map_insert theorem

 [DecidableEq α] [DecidableEq β] (f : α ↪ β) (a : α) (s : Finset α) : (insert a s).map f = insert (f a) (s.map f)

Full source

@[simp]
theorem map_insert [DecidableEq α] [DecidableEq β] (f : α ↪ β) (a : α) (s : Finset α) :
    (insert a s).map f = insert (f a) (s.map f) := by
  simp only [insert_eq, map_union, map_singleton]

Image of Inserted Finite Set under Injective Embedding: $f(\text{insert}(a, s)) = \text{insert}(f(a), f(s))$

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality, and let $f : \alpha \hookrightarrow \beta$ be an injective function embedding. For any element $a \in \alpha$ and any finite set $s \subseteq \alpha$, the image of the finite set $\text{insert}(a, s)$ under $f$ is equal to $\text{insert}(f(a), s.map(f))$.

Finset.map_cons theorem

 (f : α ↪ β) (a : α) (s : Finset α) (ha : a ∉ s) : (cons a s ha).map f = cons (f a) (s.map f) (by simpa using ha)

Full source

@[simp]
theorem map_cons (f : α ↪ β) (a : α) (s : Finset α) (ha : a ∉ s) :
    (cons a s ha).map f = cons (f a) (s.map f) (by simpa using ha) :=
  eq_of_veq <| Multiset.map_cons f a s.val

Image of a Cons-Constructed Finite Set Under an Injective Embedding

Informal description

Let $f : \alpha \hookrightarrow \beta$ be an injective function embedding, $a \in \alpha$ an element, and $s$ a finite subset of $\alpha$ such that $a \notin s$. Then the image of the finite set $\text{cons}(a, s, ha)$ under $f$ is equal to $\text{cons}(f(a), s.map(f), h)$, where $h$ is the proof that $f(a) \notin s.map(f)$ derived from $ha$.

Finset.map_eq_empty theorem

: s.map f = ∅ ↔ s = ∅

Full source

@[simp]
theorem map_eq_empty : s.map f = ∅ ↔ s = ∅ := (map_injective f).eq_iff' (map_empty f)

Empty Set Image Equivalence under Injective Embedding: $f(s) = \emptyset \iff s = \emptyset$

Informal description

For any injective function embedding $f : \alpha \hookrightarrow \beta$ and any finite set $s \subseteq \alpha$, the image of $s$ under $f$ is empty if and only if $s$ is empty. In other words, $f(s) = \emptyset \leftrightarrow s = \emptyset$.

Finset.map_nonempty theorem

: (s.map f).Nonempty ↔ s.Nonempty

Full source

@[simp]
theorem map_nonempty : (s.map f).Nonempty ↔ s.Nonempty :=
  mod_cast Set.image_nonempty (f := f) (s := s)

Nonempty Image Equivalence for Finite Sets under Injective Embedding: $f(s) \neq \emptyset \iff s \neq \emptyset$

Informal description

For any injective function embedding $f \colon \alpha \hookrightarrow \beta$ and any finite set $s \subseteq \alpha$, the image $f(s)$ is nonempty if and only if $s$ is nonempty.

Finset.map_nontrivial theorem

: (s.map f).Nontrivial ↔ s.Nontrivial

Full source

@[simp]
theorem map_nontrivial : (s.map f).Nontrivial ↔ s.Nontrivial :=
  mod_cast Set.image_nontrivial f.injective (s := s)

Nontriviality of Finite Set Image under Injective Embedding: $f(s)$ is Nontrivial $\iff$ $s$ is Nontrivial

Informal description

For any injective function embedding $f \colon \alpha \hookrightarrow \beta$ and any finite set $s \subseteq \alpha$, the image $f(s)$ is nontrivial (i.e., contains at least two distinct elements) if and only if $s$ is nontrivial (i.e., contains at least two distinct elements).

Finset.attach_map_val theorem

{s : Finset α} : s.attach.map (Embedding.subtype _) = s

Full source

theorem attach_map_val {s : Finset α} : s.attach.map (Embedding.subtype _) = s :=
  eq_of_veq <| by rw [map_val, attach_val]; exact Multiset.attach_map_val _

Image of Attached Set under Subtype Inclusion Equals Original Set

Informal description

For any finite set $s$ of elements of type $\alpha$, the image of the attached set $s.\text{attach}$ under the subtype inclusion embedding is equal to $s$ itself. That is, mapping the elements of $s.\text{attach}$ (which are pairs $(x, h_x)$ where $h_x$ is a proof that $x \in s$) back to their underlying values via the inclusion map recovers the original finite set $s$.

Finset.range_add_one' theorem

(n : ℕ) : range (n + 1) = insert 0 ((range n).map ⟨fun i => i + 1, fun i j => by simp⟩)

Full source

theorem range_add_one' (n : ℕ) :
    range (n + 1) = insert 0 ((range n).map ⟨fun i => i + 1, fun i j => by simp⟩) := by
  ext (⟨⟩ | ⟨n⟩) <;> simp [Nat.zero_lt_succ n]

Range Construction via Successor Map: $\text{range}(n+1) = \{0\} \cup (\text{range}(n) + 1)$

Informal description

For any natural number $n$, the finite set $\{0, 1, \ldots, n\}$ is equal to the union of $\{0\}$ with the image of $\{0, 1, \ldots, n-1\}$ under the injective function $i \mapsto i + 1$.

Finset.image definition

(f : α → β) (s : Finset α) : Finset β

Full source

/-- `image f s` is the forward image of `s` under `f`. -/
def image (f : α → β) (s : Finset α) : Finset β :=
  (s.1.map f).toFinset

Image of a finite set under a function

Informal description

Given a function $f : \alpha \to \beta$ and a finite set $s$ of type $\alpha$, the image of $s$ under $f$ is the finite set in $\beta$ obtained by applying $f$ to each element of $s$ and removing duplicates.

Finset.image_val theorem

(f : α → β) (s : Finset α) : (image f s).1 = (s.1.map f).dedup

Full source

@[simp]
theorem image_val (f : α → β) (s : Finset α) : (image f s).1 = (s.1.map f).dedup :=
  rfl

Image Construction via Deduplication of Mapped Multiset

Informal description

For any function $f : \alpha \to \beta$ and finite set $s \subseteq \alpha$, the underlying multiset of the image $s.image f$ is equal to the deduplicated version of the multiset obtained by applying $f$ to each element of the underlying multiset of $s$. That is, $(s.image f).val = (s.val.map f).dedup$.

Finset.image_empty theorem

(f : α → β) : (∅ : Finset α).image f = ∅

Full source

@[simp]
theorem image_empty (f : α → β) : (∅ : Finset α).image f = ∅ :=
  rfl

Image of Empty Set is Empty

Informal description

For any function $f : \alpha \to \beta$, the image of the empty finite set under $f$ is the empty set, i.e., $f(\emptyset) = \emptyset$.

Finset.mem_image theorem

: b ∈ s.image f ↔ ∃ a ∈ s, f a = b

Full source

@[simp]
theorem mem_image : b ∈ s.image fb ∈ s.image f ↔ ∃ a ∈ s, f a = b := by
  simp only [mem_def, image_val, mem_dedup, Multiset.mem_map, exists_prop]

Characterization of Membership in Image of Finite Set

Informal description

For any function $f : \alpha \to \beta$ and finite set $s \subseteq \alpha$, an element $b \in \beta$ belongs to the image $f(s)$ if and only if there exists an element $a \in s$ such that $f(a) = b$.

Finset.mem_image_of_mem theorem

(f : α → β) {a} (h : a ∈ s) : f a ∈ s.image f

Full source

theorem mem_image_of_mem (f : α → β) {a} (h : a ∈ s) : f a ∈ s.image f :=
  mem_image.2 ⟨_, h, rfl⟩

Image of Element in Finite Set is in Image of Set

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in s$ where $s$ is a finite subset of $\alpha$, the image $f(a)$ belongs to the image of $s$ under $f$, i.e., $f(a) \in f(s)$.

Finset.forall_mem_image theorem

{p : β → Prop} : (∀ y ∈ s.image f, p y) ↔ ∀ ⦃x⦄, x ∈ s → p (f x)

Full source

lemma forall_mem_image {p : β → Prop} : (∀ y ∈ s.image f, p y) ↔ ∀ ⦃x⦄, x ∈ s → p (f x) := by simp

Universal Quantification over Image of Finite Set

Informal description

For any predicate $p : \beta \to \text{Prop}$, the following are equivalent: 1. For all $y$ in the image of the finite set $s$ under the function $f : \alpha \to \beta$, the predicate $p(y)$ holds. 2. For all $x \in s$, the predicate $p(f(x))$ holds. In other words: $$(\forall y \in f(s),\, p(y)) \leftrightarrow (\forall x \in s,\, p(f(x)))$$

Finset.exists_mem_image theorem

{p : β → Prop} : (∃ y ∈ s.image f, p y) ↔ ∃ x ∈ s, p (f x)

Full source

lemma exists_mem_image {p : β → Prop} : (∃ y ∈ s.image f, p y) ↔ ∃ x ∈ s, p (f x) := by simp

Existence in Image of Finite Set Under Function

Informal description

For any predicate $p : \beta \to \text{Prop}$, there exists an element $y$ in the image of the finite set $s$ under the function $f : \alpha \to \beta$ such that $p(y)$ holds if and only if there exists an element $x \in s$ such that $p(f(x))$ holds. In other words: $$(\exists y \in f(s),\, p(y)) \leftrightarrow (\exists x \in s,\, p(f(x)))$$

Finset.map_eq_image theorem

(f : α ↪ β) (s : Finset α) : s.map f = s.image f

Full source

theorem map_eq_image (f : α ↪ β) (s : Finset α) : s.map f = s.image f :=
  eq_of_veq (s.map f).2.dedup.symm

Equality of Map and Image for Finite Sets under Injective Embedding

Informal description

For any injective function embedding $f : \alpha \hookrightarrow \beta$ and any finite set $s$ of type $\alpha$, the image of $s$ under $f$ via the `map` operation is equal to the image of $s$ under $f$ via the `image` operation. In other words: $$f(s)_{\text{map}} = f(s)_{\text{image}}$$

Finset.mem_image_const theorem

: c ∈ s.image (const α b) ↔ s.Nonempty ∧ b = c

Full source

theorem mem_image_const : c ∈ s.image (const α b)c ∈ s.image (const α b) ↔ s.Nonempty ∧ b = c := by
  rw [mem_image]
  simp only [exists_prop, const_apply, exists_and_right]
  rfl

Membership in Image of Constant Function on Finite Set

Informal description

For a finite set $s$ of type $\alpha$ and elements $b, c$ of type $\beta$, the element $c$ belongs to the image of $s$ under the constant function $\text{const}_\alpha b$ (which maps every element of $\alpha$ to $b$) if and only if $s$ is nonempty and $b = c$. In other words: $$c \in \text{image}(\text{const}_\alpha b)(s) \leftrightarrow s \neq \emptyset \land b = c$$

Finset.mem_image_const_self theorem

: b ∈ s.image (const α b) ↔ s.Nonempty

Full source

theorem mem_image_const_self : b ∈ s.image (const α b)b ∈ s.image (const α b) ↔ s.Nonempty :=
  mem_image_const.trans <| and_iff_left rfl

Membership of Constant Value in Image of Nonempty Finite Set

Informal description

For a finite set $s$ of type $\alpha$ and an element $b$ of type $\beta$, the element $b$ belongs to the image of $s$ under the constant function $\text{const}_\alpha b$ (which maps every element of $\alpha$ to $b$) if and only if $s$ is nonempty. In other words: $$b \in \text{image}(\text{const}_\alpha b)(s) \leftrightarrow s \neq \emptyset$$

Finset.canLift instance

(c) (p) [CanLift β α c p] : CanLift (Finset β) (Finset α) (image c) fun s => ∀ x ∈ s, p x

Full source

instance canLift (c) (p) [CanLift β α c p] :
    CanLift (Finset β) (Finset α) (image c) fun s => ∀ x ∈ s, p x where
  prf := by
    rintro ⟨⟨l⟩, hd : l.Nodup⟩ hl
    lift l to List α using hl
    exact ⟨⟨l, hd.of_map _⟩, ext fun a => by simp⟩

Lifting Condition for Finite Sets via Image

Informal description

For any types $\alpha$ and $\beta$ with a lifting condition specified by `CanLift β α c p`, where $c : \alpha \to \beta$ is the lifting function and $p : \beta \to \text{Prop}$ is the condition, the finite set type `Finset β` can be lifted to `Finset α` via the function `image c`, provided that every element $x$ in the finite set satisfies $p(x)$. In other words, if every element of a finite set can be lifted from $\beta$ to $\alpha$ under condition $p$, then the entire finite set can be lifted to a finite set over $\alpha$ using the image function $c$.

Finset.image_congr theorem

(h : (s : Set α).EqOn f g) : Finset.image f s = Finset.image g s

Full source

theorem image_congr (h : (s : Set α).EqOn f g) : Finset.image f s = Finset.image g s := by
  ext
  simp_rw [mem_image, ← bex_def]
  exact exists₂_congr fun x hx => by rw [h hx]

Image Equality for Functions Equal on a Finite Set

Informal description

For any finite set $s \subseteq \alpha$ and functions $f, g : \alpha \to \beta$, if $f$ and $g$ are equal on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then the image of $s$ under $f$ equals the image of $s$ under $g$.

Function.Injective.mem_finset_image theorem

(hf : Injective f) : f a ∈ s.image f ↔ a ∈ s

Full source

theorem _root_.Function.Injective.mem_finset_image (hf : Injective f) :
    f a ∈ s.image ff a ∈ s.image f ↔ a ∈ s := by
  refine ⟨fun h => ?_, Finset.mem_image_of_mem f⟩
  obtain ⟨y, hy, heq⟩ := mem_image.1 h
  exact hf heq ▸ hy

Injective Function Preserves Membership in Finite Set Image

Informal description

For any injective function $f : \alpha \to \beta$ and any finite set $s \subseteq \alpha$, an element $f(a)$ belongs to the image of $s$ under $f$ if and only if $a$ belongs to $s$. In other words, $f(a) \in f(s) \leftrightarrow a \in s$.

Finset.coe_image theorem

: ↑(s.image f) = f '' ↑s

Full source

@[simp, norm_cast]
theorem coe_image : ↑(s.image f) = f '' ↑s :=
  Set.ext <| by simp only [mem_coe, mem_image, Set.mem_image, implies_true]

Equality of Coerced Finite Image and Set Image: $\overline{s.\text{image}(f)} = f[\overline{s}]$

Informal description

For any function $f : \alpha \to \beta$ and finite set $s \subseteq \alpha$, the image of $s$ under $f$ as a set (obtained by coercion) equals the set-theoretic image of $s$ under $f$, i.e., $\overline{s.\text{image}(f)} = f[\overline{s}]$ where $\overline{\cdot}$ denotes the coercion from finite sets to sets and $f[\cdot]$ denotes the set image.

Finset.image_nonempty theorem

: (s.image f).Nonempty ↔ s.Nonempty

Full source

@[simp]
lemma image_nonempty : (s.image f).Nonempty ↔ s.Nonempty :=
  mod_cast Set.image_nonempty (f := f) (s := (s : Set α))

Nonempty Image Equivalence for Finite Sets: $f(s) \neq \emptyset \iff s \neq \emptyset$

Informal description

For any function $f : \alpha \to \beta$ and finite set $s \subseteq \alpha$, the image $f(s)$ is nonempty if and only if $s$ is nonempty.

Finset.Nonempty.image theorem

(h : s.Nonempty) (f : α → β) : (s.image f).Nonempty

Full source

@[aesop safe apply (rule_sets := [finsetNonempty])]
protected theorem Nonempty.image (h : s.Nonempty) (f : α → β) : (s.image f).Nonempty :=
  image_nonempty.2 h

Nonempty Image of Nonempty Finite Set

Informal description

For any nonempty finite set $s \subseteq \alpha$ and any function $f : \alpha \to \beta$, the image of $s$ under $f$ is nonempty.

Finset.image_toFinset theorem

[DecidableEq α] {s : Multiset α} : s.toFinset.image f = (s.map f).toFinset

Full source

theorem image_toFinset [DecidableEq α] {s : Multiset α} :
    s.toFinset.image f = (s.map f).toFinset :=
  ext fun _ => by simp only [mem_image, Multiset.mem_toFinset, exists_prop, Multiset.mem_map]

Image of Finite Set from Multiset Equals Finite Set of Mapped Multiset

Informal description

For any multiset $s$ of elements of type $\alpha$ with decidable equality, the image of the finite set corresponding to $s$ under a function $f : \alpha \to \beta$ is equal to the finite set corresponding to the multiset obtained by applying $f$ to each element of $s$.

Finset.image_val_of_injOn theorem

(H : Set.InjOn f s) : (image f s).1 = s.1.map f

Full source

theorem image_val_of_injOn (H : Set.InjOn f s) : (image f s).1 = s.1.map f :=
  (s.2.map_on H).dedup

Image of Finite Set Under Injective Function Preserves Multiset Structure

Informal description

Let $f : \alpha \to \beta$ be a function and $s$ be a finite subset of $\alpha$. If $f$ is injective on $s$, then the underlying multiset of the image of $s$ under $f$ is equal to the multiset obtained by applying $f$ to each element of $s$ (without deduplication).

Finset.image_id theorem

[DecidableEq α] : s.image id = s

Full source

@[simp]
theorem image_id [DecidableEq α] : s.image id = s :=
  ext fun _ => by simp only [mem_image, exists_prop, id, exists_eq_right]

Image of Finite Set Under Identity Function is Itself

Informal description

For any finite set $s$ of type $\alpha$ with decidable equality, the image of $s$ under the identity function is equal to $s$ itself, i.e., $\text{image}(\text{id}, s) = s$.

Finset.image_id' theorem

[DecidableEq α] : (s.image fun x => x) = s

Full source

@[simp]
theorem image_id' [DecidableEq α] : (s.image fun x => x) = s :=
  image_id

Image of Finite Set Under Identity Function is Itself (Lambda Form)

Informal description

For any finite set $s$ of type $\alpha$ with decidable equality, the image of $s$ under the identity function (defined as $\lambda x, x$) is equal to $s$ itself, i.e., $s.\text{image}\, (\lambda x, x) = s$.

Finset.image_image theorem

[DecidableEq γ] {g : β → γ} : (s.image f).image g = s.image (g ∘ f)

Full source

theorem image_image [DecidableEq γ] {g : β → γ} : (s.image f).image g = s.image (g ∘ f) :=
  eq_of_veq <| by simp only [image_val, dedup_map_dedup_eq, Multiset.map_map]

Composition of Images for Finite Sets: $(f \circ g)[S] = f[g[S]]$

Informal description

For any finite set $s$ of type $\alpha$ and functions $f : \alpha \to \beta$ and $g : \beta \to \gamma$, the image of the image of $s$ under $f$ under $g$ is equal to the image of $s$ under the composition $g \circ f$. That is, $(s.\text{image}\, f).\text{image}\, g = s.\text{image}\, (g \circ f)$.

Finset.image_comm theorem

 {β'} [DecidableEq β'] [DecidableEq γ] {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ}
  (h_comm : ∀ a, f (g a) = g' (f' a)) : (s.image g).image f = (s.image f').image g'

Full source

theorem image_comm {β'} [DecidableEq β'] [DecidableEq γ] {f : β → γ} {g : α → β} {f' : α → β'}
    {g' : β' → γ} (h_comm : ∀ a, f (g a) = g' (f' a)) :
    (s.image g).image f = (s.image f').image g' := by simp_rw [image_image, comp_def, h_comm]

Commutativity of Image Composition for Finite Sets: $(f \circ g)[S] = (g' \circ f')[S]$

Informal description

Let $s$ be a finite set of type $\alpha$, and let $f : \beta \to \gamma$, $g : \alpha \to \beta$, $f' : \alpha \to \beta'$, and $g' : \beta' \to \gamma$ be functions such that for every $a \in \alpha$, $f(g(a)) = g'(f'(a))$. Then the image of the image of $s$ under $g$ under $f$ is equal to the image of the image of $s$ under $f'$ under $g'$. That is, $(s.\text{image}\, g).\text{image}\, f = (s.\text{image}\, f').\text{image}\, g'$.

Function.Semiconj.finset_image theorem

 [DecidableEq α] {f : α → β} {ga : α → α} {gb : β → β} (h : Function.Semiconj f ga gb) :
  Function.Semiconj (image f) (image ga) (image gb)

Full source

theorem _root_.Function.Semiconj.finset_image [DecidableEq α] {f : α → β} {ga : α → α} {gb : β → β}
    (h : Function.Semiconj f ga gb) : Function.Semiconj (image f) (image ga) (image gb) := fun _ =>
  image_comm h

Semiconjugacy of Image Operations: $f \circ g_a = g_b \circ f$ implies $\text{image}\, f \circ \text{image}\, g_a = \text{image}\, g_b \circ \text{image}\, f$

Informal description

Let $f : \alpha \to \beta$ be a function that semiconjugates $g_a : \alpha \to \alpha$ and $g_b : \beta \to \beta$, i.e., $f \circ g_a = g_b \circ f$. Then for any finite set $s \subseteq \alpha$, the image operation under $f$ semiconjugates the image operations under $g_a$ and $g_b$, i.e., $\text{image}\, f \circ \text{image}\, g_a = \text{image}\, g_b \circ \text{image}\, f$.

Function.Commute.finset_image theorem

[DecidableEq α] {f g : α → α} (h : Function.Commute f g) : Function.Commute (image f) (image g)

Full source

theorem _root_.Function.Commute.finset_image [DecidableEq α] {f g : α → α}
    (h : Function.Commute f g) : Function.Commute (image f) (image g) :=
  Function.Semiconj.finset_image h

Commutation of Image Operations for Commuting Functions: $f \circ g = g \circ f$ implies $f(g(S)) = g(f(S))$ for finite $S$

Informal description

Let $f, g : \alpha \to \alpha$ be commuting functions (i.e., $f \circ g = g \circ f$). Then for any finite set $s \subseteq \alpha$, the image operations under $f$ and $g$ commute, i.e., $f(g(s)) = g(f(s))$ where $f(s)$ denotes the image of $s$ under $f$.

Finset.image_subset_image theorem

{s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₁.image f ⊆ s₂.image f

Full source

theorem image_subset_image {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₁.image f ⊆ s₂.image f := by
  simp only [subset_def, image_val, subset_dedup', dedup_subset', Multiset.map_subset_map h]

Image Preserves Subset Relation for Finite Sets

Informal description

For any two finite sets $s_1$ and $s_2$ of type $\alpha$ such that $s_1 \subseteq s_2$, and for any function $f : \alpha \to \beta$, the image of $s_1$ under $f$ is a subset of the image of $s_2$ under $f$, i.e., $f(s_1) \subseteq f(s_2)$.

Finset.image_subset_iff theorem

: s.image f ⊆ t ↔ ∀ x ∈ s, f x ∈ t

Full source

theorem image_subset_iff : s.image f ⊆ ts.image f ⊆ t ↔ ∀ x ∈ s, f x ∈ t :=
  calc
    s.image f ⊆ t ↔ f '' ↑s ⊆ ↑t := by norm_cast
    _ ↔ _ := Set.image_subset_iff

Image Subset Criterion for Finite Sets: $f(s) \subseteq t \leftrightarrow \forall x \in s, f(x) \in t$

Informal description

For any function $f \colon \alpha \to \beta$, finite set $s \subseteq \alpha$, and set $t \subseteq \beta$, the image of $s$ under $f$ is a subset of $t$ if and only if for every element $x \in s$, we have $f(x) \in t$. In symbols: \[ f(s) \subseteq t \leftrightarrow \forall x \in s, f(x) \in t. \]

Finset.image_mono theorem

(f : α → β) : Monotone (Finset.image f)

Full source

theorem image_mono (f : α → β) : Monotone (Finset.image f) := fun _ _ => image_subset_image

Monotonicity of Finite Set Image Operation

Informal description

For any function $f : \alpha \to \beta$, the image operation $\text{image}(f) : \text{Finset} \alpha \to \text{Finset} \beta$ is monotone with respect to the subset relation $\subseteq$. That is, for any finite sets $s_1, s_2 \subseteq \alpha$, if $s_1 \subseteq s_2$, then $f(s_1) \subseteq f(s_2)$.

Finset.image_injective theorem

(hf : Injective f) : Injective (image f)

Full source

lemma image_injective (hf : Injective f) : Injective (image f) := by
  simpa only [funext (map_eq_image _)] using map_injective ⟨f, hf⟩

Injectivity of Finite Set Image Operation under Injective Function

Informal description

If a function $f \colon \alpha \to \beta$ is injective, then the image operation $\text{image}(f) \colon \text{Finset} \alpha \to \text{Finset} \beta$ is also injective. That is, for any finite sets $s_1, s_2 \subseteq \alpha$, if $f(s_1) = f(s_2)$, then $s_1 = s_2$.

Finset.image_inj theorem

{t : Finset α} (hf : Injective f) : s.image f = t.image f ↔ s = t

Full source

lemma image_inj {t : Finset α} (hf : Injective f) : s.image f = t.image f ↔ s = t :=
  (image_injective hf).eq_iff

Equality of Images under Injective Function Reflects Equality of Finite Sets

Informal description

For any injective function $f \colon \alpha \to \beta$ and finite sets $s, t \subseteq \alpha$, the images $f(s)$ and $f(t)$ are equal if and only if $s = t$.

Finset.image_subset_image_iff theorem

{t : Finset α} (hf : Injective f) : s.image f ⊆ t.image f ↔ s ⊆ t

Full source

theorem image_subset_image_iff {t : Finset α} (hf : Injective f) :
    s.image f ⊆ t.image fs.image f ⊆ t.image f ↔ s ⊆ t :=
  mod_cast Set.image_subset_image_iff hf (s := s) (t := t)

Image Subset Relation under Injective Function: $f(s) \subseteq f(t) \leftrightarrow s \subseteq t$

Informal description

For any injective function $f \colon \alpha \to \beta$ and finite sets $s, t \subseteq \alpha$, the image of $s$ under $f$ is a subset of the image of $t$ under $f$ if and only if $s$ is a subset of $t$. In symbols: $$ f(s) \subseteq f(t) \leftrightarrow s \subseteq t $$

Finset.image_ssubset_image theorem

{t : Finset α} (hf : Injective f) : s.image f ⊂ t.image f ↔ s ⊂ t

Full source

lemma image_ssubset_image {t : Finset α} (hf : Injective f) : s.image f ⊂ t.image fs.image f ⊂ t.image f ↔ s ⊂ t := by
  simp_rw [← lt_iff_ssubset]
  exact lt_iff_lt_of_le_iff_le' (image_subset_image_iff hf) (image_subset_image_iff hf)

Strict Image Subset Relation under Injective Function: $f(s) \subset f(t) \leftrightarrow s \subset t$

Informal description

For any injective function $f \colon \alpha \to \beta$ and finite sets $s, t \subseteq \alpha$, the image of $s$ under $f$ is a strict subset of the image of $t$ under $f$ if and only if $s$ is a strict subset of $t$. In symbols: $$ f(s) \subset f(t) \leftrightarrow s \subset t $$

Finset.coe_image_subset_range theorem

: ↑(s.image f) ⊆ Set.range f

Full source

theorem coe_image_subset_range : ↑(s.image f) ⊆ Set.range f :=
  calc
    ↑(s.image f) = f '' ↑s := coe_image
    _ ⊆ Set.range f := Set.image_subset_range f ↑s

Image of Finite Set is Subset of Range: $f(s) \subseteq \text{range}(f)$

Informal description

For any function $f : \alpha \to \beta$ and finite set $s \subseteq \alpha$, the image of $s$ under $f$ (as a set) is a subset of the range of $f$, i.e., $f(s) \subseteq \text{range}(f)$.

Finset.filter_image theorem

{p : β → Prop} [DecidablePred p] : (s.image f).filter p = (s.filter fun a ↦ p (f a)).image f

Full source

theorem filter_image {p : β → Prop} [DecidablePred p] :
    (s.image f).filter p = (s.filter fun a ↦ p (f a)).image f :=
  ext fun b => by
    simp only [mem_filter, mem_image, exists_prop]
    exact
      ⟨by rintro ⟨⟨x, h1, rfl⟩, h2⟩; exact ⟨x, ⟨h1, h2⟩, rfl⟩,
       by rintro ⟨x, ⟨h1, h2⟩, rfl⟩; exact ⟨⟨x, h1, rfl⟩, h2⟩⟩

Filter-Image Commutation for Finite Sets

Informal description

For any finite set $s$ of type $\alpha$, a function $f : \alpha \to \beta$, and a decidable predicate $p : \beta \to \text{Prop}$, the following equality holds: \[ \{y \in f(s) \mid p(y)\} = f(\{x \in s \mid p(f(x))\}) \] where $f(s)$ denotes the image of $s$ under $f$.

Finset.fiber_nonempty_iff_mem_image theorem

{y : β} : (s.filter (f · = y)).Nonempty ↔ y ∈ s.image f

Full source

theorem fiber_nonempty_iff_mem_image {y : β} : (s.filter (f · = y)).Nonempty ↔ y ∈ s.image f := by
  simp [Finset.Nonempty]

Nonempty Fiber Condition for Membership in Finite Set Image

Informal description

For any finite set $s$ of type $\alpha$, a function $f : \alpha \to \beta$, and an element $y \in \beta$, the following are equivalent: 1. The set $\{x \in s \mid f(x) = y\}$ is nonempty. 2. The element $y$ belongs to the image of $s$ under $f$, i.e., $y \in f(s)$.

Finset.image_union theorem

[DecidableEq α] {f : α → β} (s₁ s₂ : Finset α) : (s₁ ∪ s₂).image f = s₁.image f ∪ s₂.image f

Full source

theorem image_union [DecidableEq α] {f : α → β} (s₁ s₂ : Finset α) :
    (s₁ ∪ s₂).image f = s₁.image f ∪ s₂.image f :=
  mod_cast Set.image_union f s₁ s₂

Image of Union Equals Union of Images for Finite Sets

Informal description

For any function $f : \alpha \to \beta$ and finite sets $s_1, s_2 \subseteq \alpha$ (with decidable equality on $\alpha$), the image of the union $s_1 \cup s_2$ under $f$ equals the union of the images: \[ f(s_1 \cup s_2) = f(s_1) \cup f(s_2) \]

Finset.image_inter_subset theorem

[DecidableEq α] (f : α → β) (s t : Finset α) : (s ∩ t).image f ⊆ s.image f ∩ t.image f

Full source

theorem image_inter_subset [DecidableEq α] (f : α → β) (s t : Finset α) :
    (s ∩ t).image f ⊆ s.image f ∩ t.image f :=
  (image_mono f).map_inf_le s t

Image of Intersection is Subset of Intersection of Images

Informal description

For any function $f : \alpha \to \beta$ and finite sets $s, t \subseteq \alpha$, the image of the intersection $s \cap t$ under $f$ is a subset of the intersection of the images, i.e., $f(s \cap t) \subseteq f(s) \cap f(t)$.

Finset.image_inter_of_injOn theorem

 [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Set.InjOn f (s ∪ t)) : (s ∩ t).image f = s.image f ∩ t.image f

Full source

theorem image_inter_of_injOn [DecidableEq α] {f : α → β} (s t : Finset α)
    (hf : Set.InjOn f (s ∪ t)) : (s ∩ t).image f = s.image f ∩ t.image f :=
  coe_injective <| by
    push_cast
    exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb

Image of Intersection Equals Intersection of Images under Injectivity Condition on Union

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality on $\alpha$, and let $f : \alpha \to \beta$ be a function. For any finite sets $s, t \subseteq \alpha$, if $f$ is injective on $s \cup t$, then the image of the intersection $s \cap t$ under $f$ equals the intersection of the images of $s$ and $t$ under $f$, i.e., \[ f(s \cap t) = f(s) \cap f(t). \]

Finset.image_inter theorem

[DecidableEq α] (s₁ s₂ : Finset α) (hf : Injective f) : (s₁ ∩ s₂).image f = s₁.image f ∩ s₂.image f

Full source

theorem image_inter [DecidableEq α] (s₁ s₂ : Finset α) (hf : Injective f) :
    (s₁ ∩ s₂).image f = s₁.image f ∩ s₂.image f :=
  image_inter_of_injOn _ _ hf.injOn

Image of Intersection Equals Intersection of Images for Injective Functions

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality on $\alpha$, and let $f : \alpha \to \beta$ be an injective function. For any finite sets $s_1, s_2 \subseteq \alpha$, the image of their intersection under $f$ equals the intersection of their images, i.e., \[ f(s_1 \cap s_2) = f(s_1) \cap f(s_2). \]

Finset.image_singleton theorem

(f : α → β) (a : α) : image f { a } = {f a}

Full source

@[simp]
theorem image_singleton (f : α → β) (a : α) : image f {a} = {f a} :=
  ext fun x => by simpa only [mem_image, exists_prop, mem_singleton, exists_eq_left] using eq_comm

Image of Singleton Set is Singleton of Image

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, the image of the singleton set $\{a\}$ under $f$ is the singleton set $\{f(a)\}$.

Finset.image_insert theorem

[DecidableEq α] (f : α → β) (a : α) (s : Finset α) : (insert a s).image f = insert (f a) (s.image f)

Full source

@[simp]
theorem image_insert [DecidableEq α] (f : α → β) (a : α) (s : Finset α) :
    (insert a s).image f = insert (f a) (s.image f) := by
  simp only [insert_eq, image_singleton, image_union]

Image of Inserted Element Equals Inserted Image

Informal description

For any function $f : \alpha \to \beta$, element $a \in \alpha$, and finite set $s \subseteq \alpha$ (with decidable equality on $\alpha$), the image of the set $\{a\} \cup s$ under $f$ is equal to $\{f(a)\} \cup f(s)$. In symbols: \[ f(\{a\} \cup s) = \{f(a)\} \cup f(s) \]

Finset.erase_image_subset_image_erase theorem

[DecidableEq α] (f : α → β) (s : Finset α) (a : α) : (s.image f).erase (f a) ⊆ (s.erase a).image f

Full source

theorem erase_image_subset_image_erase [DecidableEq α] (f : α → β) (s : Finset α) (a : α) :
    (s.image f).erase (f a) ⊆ (s.erase a).image f := by
  simp only [subset_iff, and_imp, exists_prop, mem_image, exists_imp, mem_erase]
  rintro b hb x hx rfl
  exact ⟨_, ⟨ne_of_apply_ne f hb, hx⟩, rfl⟩

Image of Erased Set Contains Erased Image

Informal description

For any function $f : \alpha \to \beta$ and finite set $s \subseteq \alpha$, the image of $s$ under $f$ with $f(a)$ removed is a subset of the image of $s$ with $a$ removed under $f$. In other words, $(f[s] \setminus \{f(a)\}) \subseteq f[s \setminus \{a\}]$.

Finset.image_erase theorem

 [DecidableEq α] {f : α → β} (hf : Injective f) (s : Finset α) (a : α) : (s.erase a).image f = (s.image f).erase (f a)

Full source

@[simp]
theorem image_erase [DecidableEq α] {f : α → β} (hf : Injective f) (s : Finset α) (a : α) :
    (s.erase a).image f = (s.image f).erase (f a) :=
  coe_injective <| by push_cast [Set.image_diff hf, Set.image_singleton]; rfl

Image of Erased Set Equals Erased Image for Injective Functions

Informal description

For any injective function $f : \alpha \to \beta$, finite set $s \subseteq \alpha$, and element $a \in \alpha$, the image of the set $s \setminus \{a\}$ under $f$ is equal to the set $f(s) \setminus \{f(a)\}$. In symbols: $$ f(s \setminus \{a\}) = f(s) \setminus \{f(a)\}. $$

Finset.image_eq_empty theorem

: s.image f = ∅ ↔ s = ∅

Full source

@[simp]
theorem image_eq_empty : s.image f = ∅ ↔ s = ∅ := mod_cast Set.image_eq_empty (f := f) (s := s)

Image of Finite Set is Empty iff Domain is Empty

Informal description

For any function $f : \alpha \to \beta$ and any finite set $s \subseteq \alpha$, the image of $s$ under $f$ is empty if and only if $s$ is empty. In symbols: $$ f(s) = \emptyset \leftrightarrow s = \emptyset $$

Finset.image_sdiff theorem

[DecidableEq α] {f : α → β} (s t : Finset α) (hf : Injective f) : (s \ t).image f = s.image f \ t.image f

Full source

theorem image_sdiff [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Injective f) :
    (s \ t).image f = s.image f \ t.image f :=
  mod_cast Set.image_diff hf s t

Image of Set Difference under Injective Function on Finite Sets

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality on $\alpha$, and let $f : \alpha \to \beta$ be an injective function. For any finite subsets $s, t \subseteq \alpha$, the image of the set difference $s \setminus t$ under $f$ equals the set difference of the images, i.e., $$ f(s \setminus t) = f(s) \setminus f(t). $$

Finset.image_sdiff_of_injOn theorem

[DecidableEq α] {t : Finset α} (hf : Set.InjOn f s) (hts : t ⊆ s) : (s \ t).image f = s.image f \ t.image f

Full source

lemma image_sdiff_of_injOn [DecidableEq α] {t : Finset α} (hf : Set.InjOn f s) (hts : t ⊆ s) :
    (s \ t).image f = s.image f \ t.image f :=
  mod_cast Set.image_diff_of_injOn hf <| coe_subset.2 hts

Image of Set Difference under Injective Function

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality on $\alpha$, and let $f : \alpha \to \beta$ be a function. For any finite subsets $s, t \subseteq \alpha$ such that $f$ is injective on $s$ and $t \subseteq s$, the image of the set difference $s \setminus t$ under $f$ equals the set difference of the images, i.e., $$ f(s \setminus t) = f(s) \setminus f(t). $$

Disjoint.of_image_finset theorem

{s t : Finset α} {f : α → β} (h : Disjoint (s.image f) (t.image f)) : Disjoint s t

Full source

theorem _root_.Disjoint.of_image_finset {s t : Finset α} {f : α → β}
    (h : Disjoint (s.image f) (t.image f)) : Disjoint s t :=
  disjoint_iff_ne.2 fun _ ha _ hb =>
    ne_of_apply_ne f <| h.forall_ne_finset (mem_image_of_mem _ ha) (mem_image_of_mem _ hb)

Disjointness of Preimages via Disjoint Images

Informal description

For any finite sets $s$ and $t$ of type $\alpha$ and any function $f : \alpha \to \beta$, if the images of $s$ and $t$ under $f$ are disjoint, then $s$ and $t$ themselves are disjoint.

Finset.mem_range_iff_mem_finset_range_of_mod_eq' theorem

 [DecidableEq α] {f : ℕ → α} {a : α} {n : ℕ} (hn : 0 < n) (h : ∀ i, f (i % n) = f i) :
  a ∈ Set.range f ↔ a ∈ (Finset.range n).image fun i => f i

Full source

theorem mem_range_iff_mem_finset_range_of_mod_eq' [DecidableEq α] {f : ℕ → α} {a : α} {n : ℕ}
    (hn : 0 < n) (h : ∀ i, f (i % n) = f i) :
    a ∈ Set.range fa ∈ Set.range f ↔ a ∈ (Finset.range n).image fun i => f i := by
  constructor
  · rintro ⟨i, hi⟩
    simp only [mem_image, exists_prop, mem_range]
    exact ⟨i % n, Nat.mod_lt i hn, (rfl.congr hi).mp (h i)⟩
  · rintro h
    simp only [mem_image, exists_prop, Set.mem_range, mem_range] at *
    rcases h with ⟨i, _, ha⟩
    exact ⟨i, ha⟩

Range Membership Equivalence for Periodic Functions on Natural Numbers

Informal description

Let $f : \mathbb{N} \to \alpha$ be a function, $a \in \alpha$, and $n \in \mathbb{N}$ with $n > 0$. Suppose that for all $i \in \mathbb{N}$, $f(i \bmod n) = f(i)$. Then $a$ is in the range of $f$ if and only if $a$ is in the image of the finite set $\{0, \ldots, n-1\}$ under $f$.

Finset.mem_range_iff_mem_finset_range_of_mod_eq theorem

 [DecidableEq α] {f : ℤ → α} {a : α} {n : ℕ} (hn : 0 < n) (h : ∀ i, f (i % n) = f i) :
  a ∈ Set.range f ↔ a ∈ (Finset.range n).image (fun (i : ℕ) => f i)

Full source

theorem mem_range_iff_mem_finset_range_of_mod_eq [DecidableEq α] {f : ℤ → α} {a : α} {n : ℕ}
    (hn : 0 < n) (h : ∀ i, f (i % n) = f i) :
    a ∈ Set.range fa ∈ Set.range f ↔ a ∈ (Finset.range n).image (fun (i : ℕ) => f i) :=
  suffices (∃ i, f (i % n) = a) ↔ ∃ i, i < n ∧ f ↑i = a by simpa [h]
  have hn' : 0 < (n : ℤ) := Int.ofNat_lt.mpr hn
  Iff.intro
    (fun ⟨i, hi⟩ =>
      have : 0 ≤ i % ↑n := Int.emod_nonneg _ (ne_of_gt hn')
      ⟨Int.toNat (i % n), by
        rw [← Int.ofNat_lt, Int.toNat_of_nonneg this]; exact ⟨Int.emod_lt_of_pos i hn', hi⟩⟩)
    fun ⟨i, hi, ha⟩ =>
    ⟨i, by rw [Int.emod_eq_of_lt (Int.ofNat_zero_le _) (Int.ofNat_lt_ofNat_of_lt hi), ha]⟩

Range Membership Equivalence for Periodic Functions on Integers

Informal description

Let $f : \mathbb{Z} \to \alpha$ be a function, $a \in \alpha$, and $n \in \mathbb{N}$ with $n > 0$. Suppose that for all integers $i$, $f(i \bmod n) = f(i)$. Then $a$ is in the range of $f$ if and only if $a$ is in the image of the finite set $\{0, \ldots, n-1\}$ under the restriction of $f$ to $\mathbb{N}$.

Finset.attach_image_val theorem

[DecidableEq α] {s : Finset α} : s.attach.image Subtype.val = s

Full source

@[simp]
theorem attach_image_val [DecidableEq α] {s : Finset α} : s.attach.image Subtype.val = s :=
  eq_of_veq <| by rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]

Image of Attached Set Under Value Function Equals Original Set

Informal description

For any finite set $s$ of elements of type $\alpha$ with decidable equality, the image of the attached set $s.\text{attach}$ under the subtype value function $\text{Subtype.val}$ is equal to $s$ itself. In other words, applying the value function to the elements of $s.\text{attach}$ recovers the original finite set $s$.

Finset.attach_insert theorem

 [DecidableEq α] {a : α} {s : Finset α} :
  attach (insert a s) =
    insert (⟨a, mem_insert_self a s⟩ : { x // x ∈ insert a s }) ((attach s).image fun x => ⟨x.1, mem_insert_of_mem x.2⟩)

Full source

@[simp]
theorem attach_insert [DecidableEq α] {a : α} {s : Finset α} :
    attach (insert a s) =
      insert (⟨a, mem_insert_self a s⟩ : { x // x ∈ insert a s })
        ((attach s).image fun x => ⟨x.1, mem_insert_of_mem x.2⟩) :=
  ext fun ⟨x, hx⟩ =>
    ⟨Or.casesOn (mem_insert.1 hx)
        (fun h : x = a => fun _ => mem_insert.2 <| Or.inl <| Subtype.eq h) fun h : x ∈ s => fun _ =>
        mem_insert_of_mem <| mem_image.2 <| ⟨⟨x, h⟩, mem_attach _ _, Subtype.eq rfl⟩,
      fun _ => Finset.mem_attach _ _⟩

Attached Set of Insertion Equals Insertion of Attached Elements

Informal description

Let $\alpha$ be a type with decidable equality, $a$ an element of $\alpha$, and $s$ a finite subset of $\alpha$. Then the attached set of the finite set obtained by inserting $a$ into $s$ is equal to the finite set obtained by inserting the element $\langle a, \text{mem\_insert\_self}\ a\ s \rangle$ (which is $a$ paired with a proof that $a \in \text{insert}\ a\ s$) into the image of the attached set of $s$ under the function that maps each element $x$ of the attached set to $\langle x.1, \text{mem\_insert\_of\_mem}\ x.2 \rangle$ (which is $x$'s value paired with a proof that it is in $\text{insert}\ a\ s$).

Finset.disjoint_image theorem

{s t : Finset α} {f : α → β} (hf : Injective f) : Disjoint (s.image f) (t.image f) ↔ Disjoint s t

Full source

@[simp]
theorem disjoint_image {s t : Finset α} {f : α → β} (hf : Injective f) :
    DisjointDisjoint (s.image f) (t.image f) ↔ Disjoint s t :=
  mod_cast Set.disjoint_image_iff hf (s := s) (t := t)

Disjointness of Images under Injective Function is Equivalent to Disjointness of Preimages for Finite Sets

Informal description

For any finite sets $s, t \subseteq \alpha$ and any injective function $f : \alpha \to \beta$, the images $f(s)$ and $f(t)$ are disjoint if and only if $s$ and $t$ are disjoint. In other words, $f(s) \cap f(t) = \emptyset$ if and only if $s \cap t = \emptyset$.

Finset.image_const theorem

{s : Finset α} (h : s.Nonempty) (b : β) : (s.image fun _ => b) = singleton b

Full source

theorem image_const {s : Finset α} (h : s.Nonempty) (b : β) : (s.image fun _ => b) = singleton b :=
  mod_cast Set.Nonempty.image_const (coe_nonempty.2 h) b

Image of Nonempty Finite Set under Constant Function is Singleton

Informal description

For any nonempty finite set $s$ of type $\alpha$ and any element $b \in \beta$, the image of $s$ under the constant function $\lambda \_, b$ is the singleton finite set $\{b\}$.

Finset.map_erase theorem

[DecidableEq α] (f : α ↪ β) (s : Finset α) (a : α) : (s.erase a).map f = (s.map f).erase (f a)

Full source

@[simp]
theorem map_erase [DecidableEq α] (f : α ↪ β) (s : Finset α) (a : α) :
    (s.erase a).map f = (s.map f).erase (f a) := by
  simp_rw [map_eq_image]
  exact s.image_erase f.2 a

Image of Erased Set Equals Erased Image under Injective Embedding

Informal description

For any injective function embedding $f : \alpha \hookrightarrow \beta$, finite set $s \subseteq \alpha$, and element $a \in \alpha$, the image of the set $s \setminus \{a\}$ under $f$ is equal to the set $f(s) \setminus \{f(a)\}$. In symbols: $$ f(s \setminus \{a\}) = f(s) \setminus \{f(a)\}. $$

Finset.filterMap definition

(f : α → Option β) (s : Finset α) (f_inj : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') : Finset β

Full source

/-- `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}`. -/
-- TODO: should there be `filterImage` too?
def filterMap (f : α → Option β) (s : Finset α)
    (f_inj : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') : Finset β :=
  ⟨s.val.filterMap f, s.nodup.filterMap f f_inj⟩

Filter and map operation on finite sets

Informal description

Given a function $ f : \alpha \to \text{Option } \beta $ and a finite set $ s $ of elements of type $ \alpha $, the operation `filterMap` constructs a new finite set of elements of type $ \beta $ by applying $ f $ to each element of $ s $. If $ f(a) = \text{some } b $ for an element $ a \in s $, then $ b $ is included in the resulting finite set; otherwise, the element is excluded. The function $ f $ must satisfy the injectivity-like condition that if $ b $ is in both $ f(a) $ and $ f(a') $, then $ a = a' $. In notation, `filterMap f s` is the finite set $\{b : \beta \mid \exists a \in s, f a = \text{some } b\}$.

Finset.filterMap_val theorem

: (filterMap f s' f_inj).1 = s'.1.filterMap f

Full source

@[simp]
theorem filterMap_val : (filterMap f s' f_inj).1 = s'.1.filterMap f := rfl

Underlying Multiset of Filtered Finite Set via Option-valued Function

Informal description

For a function $f : \alpha \to \text{Option } \beta$ and a finite set $s'$ of elements of type $\alpha$, the underlying multiset of the filtered finite set $\text{filterMap } f \ s' \ f_\text{inj}$ is equal to the multiset obtained by applying $\text{filterMap } f$ to the underlying multiset of $s'$.

Finset.filterMap_empty theorem

: (∅ : Finset α).filterMap f f_inj = ∅

Full source

@[simp]
theorem filterMap_empty : (∅ : Finset α).filterMap f f_inj = ∅ := rfl

Empty Set Preservation under FilterMap Operation

Informal description

For any function $f : \alpha \to \text{Option } \beta$ satisfying the injectivity condition (that $b \in f(a) \cap f(a')$ implies $a = a'$), applying the `filterMap` operation to the empty finite set $\emptyset$ yields the empty finite set $\emptyset$ again. That is, $\text{filterMap } f \ \emptyset = \emptyset$.

Finset.mem_filterMap theorem

{b : β} : b ∈ s.filterMap f f_inj ↔ ∃ a ∈ s, f a = some b

Full source

@[simp]
theorem mem_filterMap {b : β} : b ∈ s.filterMap f f_injb ∈ s.filterMap f f_inj ↔ ∃ a ∈ s, f a = some b :=
  s.val.mem_filterMap f

Membership in Filtered Finite Set via Option-valued Function

Informal description

For any element $b \in \beta$, $b$ belongs to the finite set obtained by applying `filterMap f` to $s$ if and only if there exists an element $a \in s$ such that $f(a) = \text{some } b$.

Finset.coe_filterMap theorem

: (s.filterMap f f_inj : Set β) = {b | ∃ a ∈ s, f a = some b}

Full source

@[simp, norm_cast]
theorem coe_filterMap : (s.filterMap f f_inj : Set β) = {b | ∃ a ∈ s, f a = some b} :=
  Set.ext (by simp only [mem_coe, mem_filterMap, Option.mem_def, Set.mem_setOf_eq, implies_true])

Underlying Set of Filtered Finite Set via Option-valued Function

Informal description

For a finite set $s$ of type $\alpha$ and a function $f : \alpha \to \text{Option } \beta$ satisfying the injectivity-like condition that $b \in f(a) \cap f(a')$ implies $a = a'$, the underlying set of the filtered finite set $\text{filterMap } f \ s$ is equal to $\{b \in \beta \mid \exists a \in s, f(a) = \text{some } b\}$.

Finset.filterMap_some theorem

: s.filterMap some (by simp) = s

Full source

@[simp]
theorem filterMap_some : s.filterMap some (by simp) = s :=
  ext fun _ => by simp only [mem_filterMap, Option.some.injEq, exists_eq_right]

Identity FilterMap: $\text{filterMap some } s = s$

Informal description

For any finite set $s$ of type $\alpha$, applying the `filterMap` operation with the identity function `some : $\alpha \to \text{Option } \alpha$` (which maps each element $a$ to $\text{some } a$) returns $s$ itself, i.e., $\text{filterMap some } s = s$.

Finset.filterMap_mono theorem

(h : s ⊆ t) : filterMap f s f_inj ⊆ filterMap f t f_inj

Full source

theorem filterMap_mono (h : s ⊆ t) :
    filterMapfilterMap f s f_inj ⊆ filterMap f t f_inj := by
  rw [← val_le_iff] at h ⊢
  exact Multiset.filterMap_le_filterMap f h

Monotonicity of Filter-Map Operation on Finite Sets

Informal description

For any function $f : \alpha \to \text{Option } \beta$ satisfying the injectivity-like condition that $b \in f(a) \cap f(a')$ implies $a = a'$, and for any finite sets $s, t \subseteq \alpha$, if $s \subseteq t$, then $\text{filterMap } f \ s \subseteq \text{filterMap } f \ t$.

List.toFinset_filterMap theorem

[DecidableEq α] [DecidableEq β] (s : List α) : (s.filterMap f).toFinset = s.toFinset.filterMap f f_inj

Full source

@[simp]
theorem _root_.List.toFinset_filterMap [DecidableEq α] [DecidableEq β] (s : List α) :
    (s.filterMap f).toFinset = s.toFinset.filterMap f f_inj := by
  simp [← Finset.coe_inj]

Commutativity of `filterMap` and `toFinset` for Lists

Informal description

For any list `s` of elements of type `α` with decidable equality on both `α` and `β`, the finite set obtained by first applying the `filterMap` operation to the list and then converting to a finite set is equal to first converting the list to a finite set and then applying the `filterMap` operation. More precisely, given a function `f : α → Option β` and an injectivity condition `f_inj` (stating that if `b` is in both `f a` and `f a'`, then `a = a'`), we have: $$ \text{toFinset} (\text{filterMap } f \ s) = \text{filterMap } f \ (\text{toFinset } s) $$

Finset.subtype definition

{α} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset (Subtype p)

Full source

/-- Given a finset `s` and a predicate `p`, `s.subtype p` is the finset of `Subtype p` whose
elements belong to `s`. -/
protected def subtype {α} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset (Subtype p) :=
  (s.filter p).attach.map
    ⟨fun x => ⟨x.1, by simpa using (Finset.mem_filter.1 x.2).2⟩,
     fun _ _ H => Subtype.eq <| Subtype.mk.inj H⟩

Finite set of subtype elements

Informal description

Given a finite set $ s $ of elements of type $ \alpha $ and a decidable predicate $ p : \alpha \to \text{Prop} $, the operation `Finset.subtype p s` constructs a new finite set consisting of elements of the subtype $ \{x \mid p x\} $ whose underlying values belong to $ s $. More precisely, it first filters $ s $ to retain only elements satisfying $ p $, then attaches membership proofs to these elements, and finally maps them to the subtype while preserving the property $ p $.

Finset.mem_subtype theorem

{p : α → Prop} [DecidablePred p] {s : Finset α} : ∀ {a : Subtype p}, a ∈ s.subtype p ↔ (a : α) ∈ s

Full source

@[simp]
theorem mem_subtype {p : α → Prop} [DecidablePred p] {s : Finset α} :
    ∀ {a : Subtype p}, a ∈ s.subtype pa ∈ s.subtype p ↔ (a : α) ∈ s
  | ⟨a, ha⟩ => by simp [Finset.subtype, ha]

Membership in Subtype Finite Set

Informal description

For any decidable predicate $p : \alpha \to \text{Prop}$ and finite set $s \subseteq \alpha$, an element $a$ of the subtype $\{x \mid p x\}$ belongs to the finite set $s.\text{subtype } p$ if and only if the underlying element $(a : \alpha)$ belongs to $s$.

Finset.subtype_eq_empty theorem

{p : α → Prop} [DecidablePred p] {s : Finset α} : s.subtype p = ∅ ↔ ∀ x, p x → x ∉ s

Full source

theorem subtype_eq_empty {p : α → Prop} [DecidablePred p] {s : Finset α} :
    s.subtype p = ∅ ↔ ∀ x, p x → x ∉ s := by simp [Finset.ext_iff, Subtype.forall, Subtype.coe_mk]

Empty Subtype Finite Set Criterion

Informal description

For any decidable predicate $p : \alpha \to \text{Prop}$ and finite set $s \subseteq \alpha$, the subtype finite set $s.\text{subtype } p$ is empty if and only if no element $x \in \alpha$ satisfying $p(x)$ belongs to $s$. In other words: $$ s.\text{subtype } p = \emptyset \leftrightarrow \forall x \in \alpha, p(x) \rightarrow x \notin s $$

Finset.subtype_mono theorem

{p : α → Prop} [DecidablePred p] : Monotone (Finset.subtype p)

Full source

@[mono]
theorem subtype_mono {p : α → Prop} [DecidablePred p] : Monotone (Finset.subtype p) :=
  fun _ _ h _ hx => mem_subtype.2 <| h <| mem_subtype.1 hx

Monotonicity of Subtype Filtering on Finite Sets

Informal description

For any decidable predicate $p : \alpha \to \text{Prop}$, the function `Finset.subtype p` that maps a finite set $s \subseteq \alpha$ to the finite set $\{x \in s \mid p(x)\}$ is monotone with respect to the subset order. That is, for any finite sets $s_1, s_2 \subseteq \alpha$, if $s_1 \subseteq s_2$, then $\{x \in s_1 \mid p(x)\} \subseteq \{x \in s_2 \mid p(x)\}$.

Finset.subtype_map theorem

(p : α → Prop) [DecidablePred p] {s : Finset α} : (s.subtype p).map (Embedding.subtype _) = s.filter p

Full source

/-- `s.subtype p` converts back to `s.filter p` with
`Embedding.subtype`. -/
@[simp]
theorem subtype_map (p : α → Prop) [DecidablePred p] {s : Finset α} :
    (s.subtype p).map (Embedding.subtype _) = s.filter p := by
  ext x
  simp [@and_comm _ (_ = _), @and_left_comm _ (_ = _), @and_comm (p x) (x ∈ s)]

Subtype Image Equals Filtered Set: $\text{map}(\text{subtype}_p)(s.\text{subtype } p) = s.\text{filter } p$

Informal description

Given a decidable predicate $p : \alpha \to \text{Prop}$ and a finite set $s \subseteq \alpha$, the image of the subtype finite set $\{x \in s \mid p(x)\}$ under the inclusion embedding $\{x \mid p(x)\} \hookrightarrow \alpha$ is equal to the filtered finite set $s \text{.filter } p$.

Finset.subtype_map_of_mem theorem

 {p : α → Prop} [DecidablePred p] {s : Finset α} (h : ∀ x ∈ s, p x) : (s.subtype p).map (Embedding.subtype _) = s

Full source

/-- If all elements of a `Finset` satisfy the predicate `p`,
`s.subtype p` converts back to `s` with `Embedding.subtype`. -/
theorem subtype_map_of_mem {p : α → Prop} [DecidablePred p] {s : Finset α} (h : ∀ x ∈ s, p x) :
    (s.subtype p).map (Embedding.subtype _) = s := ext <| by simpa [subtype_map] using h

Subtype Image Equals Original Set When All Elements Satisfy Predicate

Informal description

For any decidable predicate $p : \alpha \to \text{Prop}$ and finite set $s \subseteq \alpha$, if every element $x \in s$ satisfies $p(x)$, then the image of the subtype finite set $\{x \in s \mid p(x)\}$ under the inclusion embedding $\{x \mid p(x)\} \hookrightarrow \alpha$ is equal to $s$ itself. That is: $$ \text{map}(\text{Embedding.subtype } p)(s.\text{subtype } p) = s $$

Finset.property_of_mem_map_subtype theorem

{p : α → Prop} (s : Finset { x // p x }) {a : α} (h : a ∈ s.map (Embedding.subtype _)) : p a

Full source

/-- 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 property_of_mem_map_subtype {p : α → Prop} (s : Finset { x // p x }) {a : α}
    (h : a ∈ s.map (Embedding.subtype _)) : p a := by
  rcases mem_map.1 h with ⟨x, _, rfl⟩
  exact x.2

Preservation of Subtype Property under Image Mapping

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and finite set $s$ of elements in the subtype $\{x \mid p(x)\}$, if an element $a \in \alpha$ belongs to the image of $s$ under the subtype embedding, then $p(a)$ holds. In other words: $$ a \in \text{map}(\text{Embedding.subtype } p)(s) \implies p(a) $$

Finset.not_mem_map_subtype_of_not_property theorem

{p : α → Prop} (s : Finset { x // p x }) {a : α} (h : ¬p a) : a ∉ s.map (Embedding.subtype _)

Full source

/-- 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 not_mem_map_subtype_of_not_property {p : α → Prop} (s : Finset { x // p x }) {a : α}
    (h : ¬p a) : a ∉ s.map (Embedding.subtype _) :=
  mt s.property_of_mem_map_subtype h

Non-membership in Subtype Image for Non-satisfying Elements

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and finite set $s$ of elements in the subtype $\{x \mid p(x)\}$, if an element $a \in \alpha$ does not satisfy $p(a)$, then $a$ is not in the image of $s$ under the subtype embedding. In other words: $$ \neg p(a) \implies a \notin \text{map}(\text{Embedding.subtype } p)(s) $$

Finset.map_subtype_subset theorem

{t : Set α} (s : Finset t) : ↑(s.map (Embedding.subtype _)) ⊆ t

Full source

/-- 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. -/
theorem map_subtype_subset {t : Set α} (s : Finset t) : ↑(s.map (Embedding.subtype _)) ⊆ t := by
  intro a ha
  rw [mem_coe] at ha
  convert property_of_mem_map_subtype s ha

Subtype Image is Subset of Original Set

Informal description

For any set $t$ of type $\alpha$ and any finite set $s$ of elements in the subtype $\{x \mid x \in t\}$, the image of $s$ under the subtype embedding is a subset of $t$. In other words, if we map the finite set $s$ of elements from the subtype back to $\alpha$, the resulting set is contained in $t$.

Finset.subset_set_image_iff theorem

 [DecidableEq β] {s : Set α} {t : Finset β} {f : α → β} : ↑t ⊆ f '' s ↔ ∃ s' : Finset α, ↑s' ⊆ s ∧ s'.image f = t

Full source

/-- 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 subset_set_image_iff [DecidableEq β] {s : Set α} {t : Finset β} {f : α → β} :
    ↑t ⊆ f '' s↑t ⊆ f '' s ↔ ∃ s' : Finset α, ↑s' ⊆ s ∧ s'.image f = t := by
  constructor
  · intro h
    letI : CanLift β s (f ∘ (↑)) fun y => y ∈ f '' s := ⟨fun y ⟨x, hxt, hy⟩ => ⟨⟨x, hxt⟩, hy⟩⟩
    lift t to Finset s using h
    refine ⟨t.map (Embedding.subtype _), map_subtype_subset _, ?_⟩
    ext y; simp
  · rintro ⟨t, ht, rfl⟩
    rw [coe_image]
    exact Set.image_subset f ht

Characterization of Finite Subsets of Set Images: $t \subseteq f(s) \iff \exists s' \subseteq s, f(s') = t$

Informal description

Let $s$ be a set in $\alpha$, $t$ a finite set in $\beta$, and $f : \alpha \to \beta$ a function. Then the following are equivalent: 1. The set underlying $t$ is contained in the image of $s$ under $f$, i.e., $t \subseteq f(s)$. 2. There exists a finite set $s' \subseteq \alpha$ such that $s' \subseteq s$ and the image of $s'$ under $f$ equals $t$, i.e., $f(s') = t$.

Finset.subset_image_iff theorem

 [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} : t ⊆ s.image f ↔ ∃ s' : Finset α, s' ⊆ s ∧ s'.image f = t

Full source

/--
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 subset_image_iff [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} :
    t ⊆ s.image ft ⊆ s.image f ↔ ∃ s' : Finset α, s' ⊆ s ∧ s'.image f = t := by
  simp only [← coe_subset, coe_image, subset_set_image_iff]

Characterization of Subsets of Finite Set Images

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any function $f : \alpha \to \beta$, the following are equivalent: 1. $t$ is a subset of the image of $s$ under $f$, i.e., $t \subseteq s.\text{image}(f)$. 2. There exists a finite subset $s' \subseteq s$ such that the image of $s'$ under $f$ equals $t$, i.e., $s' \subseteq s$ and $s'.\text{image}(f) = t$.

Finset.range_sdiff_zero theorem

{n : ℕ} : range (n + 1) \ {0} = (range n).image Nat.succ

Full source

theorem range_sdiff_zero {n : ℕ} : rangerange (n + 1) \ {0} = (range n).image Nat.succ := by
  induction' n with k hk
  · simp
  conv_rhs => rw [range_succ]
  rw [range_succ, image_insert, ← hk, insert_sdiff_of_not_mem]
  simp

Range Difference with Zero Equals Successor Image: $\text{range}(n+1) \setminus \{0\} = \text{succ}(\text{range}(n))$

Informal description

For any natural number $n$, the set difference between the finite set $\{0, 1, \ldots, n\}$ and the singleton set $\{0\}$ is equal to the image of the finite set $\{0, 1, \ldots, n-1\}$ under the successor function. In symbols: \[ \{0, 1, \ldots, n\} \setminus \{0\} = \{k+1 \mid k \in \{0, 1, \ldots, n-1\}\} \]

Multiset.toFinset_map theorem

[DecidableEq α] [DecidableEq β] (f : α → β) (m : Multiset α) : (m.map f).toFinset = m.toFinset.image f

Full source

theorem Multiset.toFinset_map [DecidableEq α] [DecidableEq β] (f : α → β) (m : Multiset α) :
    (m.map f).toFinset = m.toFinset.image f :=
  Finset.val_inj.1 (Multiset.dedup_map_dedup_eq _ _).symm

Equality of Mapped Multiset to Finset and Image of Finset under $f$

Informal description

For any function $f : \alpha \to \beta$ and multiset $m$ over $\alpha$, the finite set obtained by mapping $f$ over $m$ and converting to a finite set is equal to the image of $f$ applied to the finite set obtained from $m$. That is, $\text{toFinset}(\text{map}\, f\, m) = \text{image}\, f (\text{toFinset}\, m)$.

Equiv.finsetCongr definition

(e : α ≃ β) : Finset α ≃ Finset β

Full source

/-- Given an equivalence `α` to `β`, produce an equivalence between `Finset α` and `Finset β`. -/
protected def finsetCongr (e : α ≃ β) : FinsetFinset α ≃ Finset β where
  toFun s := s.map e.toEmbedding
  invFun s := s.map e.symm.toEmbedding
  left_inv s := by simp [Finset.map_map]
  right_inv s := by simp [Finset.map_map]

Equivalence of finite sets induced by a bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$, the function `Equiv.finsetCongr` constructs an equivalence between the type of finite subsets of $\alpha$ and the type of finite subsets of $\beta$. Specifically, it maps a finite set $s \subseteq \alpha$ to its image under $e$ in $\beta$, and conversely maps a finite set $t \subseteq \beta$ to its preimage under $e$ in $\alpha$.

Equiv.finsetCongr_apply theorem

(e : α ≃ β) (s : Finset α) : e.finsetCongr s = s.map e.toEmbedding

Full source

@[simp]
theorem finsetCongr_apply (e : α ≃ β) (s : Finset α) : e.finsetCongr s = s.map e.toEmbedding :=
  rfl

Image of Finite Set under Bijection Equals Map of Embedding

Informal description

Given a bijection $e : \alpha \simeq \beta$ and a finite set $s \subseteq \alpha$, the image of $s$ under the equivalence $e.\text{finsetCongr}$ is equal to the image of $s$ under the injective embedding $e.\text{toEmbedding}$. That is, $e.\text{finsetCongr}(s) = \text{map}\, e.\text{toEmbedding}\, s$.

Equiv.finsetCongr_refl theorem

: (Equiv.refl α).finsetCongr = Equiv.refl _

Full source

@[simp]
theorem finsetCongr_refl : (Equiv.refl α).finsetCongr = Equiv.refl _ := by
  ext
  simp

Finite Set Equivalence Induced by Identity Bijection is Identity

Informal description

The equivalence between finite sets induced by the identity bijection on a type $\alpha$ is equal to the identity equivalence on the type of finite subsets of $\alpha$. That is, $(\mathrm{id}_\alpha).\mathrm{finsetCongr} = \mathrm{id}_{\mathrm{Finset}\ \alpha}$.

Equiv.finsetCongr_symm theorem

(e : α ≃ β) : e.finsetCongr.symm = e.symm.finsetCongr

Full source

@[simp]
theorem finsetCongr_symm (e : α ≃ β) : e.finsetCongr.symm = e.symm.finsetCongr :=
  rfl

Inverse of Finite Set Equivalence Induced by Bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$, the inverse of the equivalence between finite sets induced by $e$ is equal to the equivalence between finite sets induced by the inverse bijection $e^{-1} : \beta \simeq \alpha$. In other words, $(e.\text{finsetCongr})^{-1} = e^{-1}.\text{finsetCongr}$.

Equiv.finsetCongr_trans theorem

(e : α ≃ β) (e' : β ≃ γ) : e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr

Full source

@[simp]
theorem finsetCongr_trans (e : α ≃ β) (e' : β ≃ γ) :
    e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr := by
  ext
  simp [-Finset.mem_map, -Equiv.trans_toEmbedding]

Composition of Finite Set Equivalences Induced by Bijections

Informal description

Given bijections $e : \alpha \simeq \beta$ and $e' : \beta \simeq \gamma$, the composition of the induced equivalences on finite sets $e.\text{finsetCongr} \circ e'.\text{finsetCongr}$ is equal to the equivalence on finite sets induced by the composition $e \circ e' : \alpha \simeq \gamma$. In other words, $(e.\text{finsetCongr}) \circ (e'.\text{finsetCongr}) = (e \circ e').\text{finsetCongr}$.

Equiv.finsetCongr_toEmbedding theorem

(e : α ≃ β) : e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding

Full source

theorem finsetCongr_toEmbedding (e : α ≃ β) :
    e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding :=
  rfl

Equality of Embeddings Induced by Bijection on Finite Sets

Informal description

Given a bijection $e : \alpha \simeq \beta$, the embedding induced by the equivalence of finite sets under $e$ is equal to the embedding obtained by applying the injective map $e$ to finite subsets of $\alpha$.

Equiv.finsetSubtypeComm definition

(p : α → Prop) : Finset { a : α // p a } ≃ { s : Finset α // ∀ a ∈ s, p a }

Full source

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

@[simps]
protected def finsetSubtypeComm (p : α → Prop) :
    FinsetFinset {a : α // p a} ≃ {s : Finset α // ∀ a ∈ s, p a} where
  toFun s := ⟨s.map ⟨fun a ↦ a.val, Subtype.val_injective⟩, fun _ h ↦
    have ⟨v, _, h⟩ := Embedding.coeFn_mk _ _ ▸ mem_map.mp h; h ▸ v.property⟩
  invFun s := s.val.attach.map (Subtype.impEmbedding _ _ s.property)
  left_inv s := by
    ext a; constructor <;> intro h <;>
    simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
      exists_and_right, exists_eq_right, Subtype.impEmbedding, Subtype.mk.injEq] at *
    · rcases h with ⟨_, ⟨_, h₁⟩, h₂⟩; exact h₂ ▸ h₁
    · use a, ⟨a.property, h⟩
  right_inv s := by
    ext a; constructor <;> intro h <;>
    simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
      exists_and_right, exists_eq_right, Subtype.impEmbedding, Subtype.mk.injEq] at *
    · rcases h with ⟨_, _, h₁, h₂⟩; exact h₂ ▸ h₁
    · use s.property _ h, a

Equivalence between finite sets of a subtype and finite sets satisfying a predicate

Informal description

Given a predicate `p : α → Prop`, there is a natural equivalence between the type of finite sets of elements of the subtype `{a : α // p a}` and the type of finite sets `s : Finset α` where every element `a ∈ s` satisfies `p a`. The forward direction maps a finite set `s` of the subtype to its image under the canonical injection `Subtype.val`, ensuring all elements satisfy `p`. The inverse direction takes a finite set `s` where all elements satisfy `p` and constructs the finite set of all elements of `s` paired with their membership proofs.

Main definitions