Mathlib.Data.Finset.Fin

Finset.attachFin definition

(s : Finset ℕ) {n : ℕ} (h : ∀ m ∈ s, m < n) : Finset (Fin n)

Full source

/-- Given a Finset `s` of `ℕ` contained in `{0,..., n-1}`, the corresponding Finset in `Fin n`
is `s.attachFin h` where `h` is a proof that all elements of `s` are less than `n`. -/
def attachFin (s : Finset ℕ) {n : ℕ} (h : ∀ m ∈ s, m < n) : Finset (Fin n) :=
  ⟨s.1.pmap (fun a ha ↦ ⟨a, ha⟩) h, s.nodup.pmap fun _ _ _ _ ↦ Fin.val_eq_of_eq⟩

Finite set of Fin elements from natural numbers

Informal description

Given a finite set $s$ of natural numbers and a natural number $n$, if every element $m \in s$ satisfies $m < n$, then $\text{attachFin}\ s\ h$ is the finite set of elements of $\text{Fin}\ n$ corresponding to the natural numbers in $s$. Here, $h$ is a proof that all elements of $s$ are less than $n$.

Finset.mem_attachFin theorem

{s : Finset ℕ} (h : ∀ m ∈ s, m < n) {a : Fin n} : a ∈ s.attachFin h ↔ (a : ℕ) ∈ s

Full source

@[simp]
theorem mem_attachFin {s : Finset ℕ} (h : ∀ m ∈ s, m < n) {a : Fin n} :
    a ∈ s.attachFin ha ∈ s.attachFin h ↔ (a : ℕ) ∈ s :=
  ⟨fun h ↦
    let ⟨_, hb₁, hb₂⟩ := Multiset.mem_pmap.1 h
    hb₂ ▸ hb₁,
    fun h ↦ Multiset.mem_pmap.2 ⟨a, h, Fin.eta _ _⟩⟩

Membership in $\text{attachFin}$ Corresponds to Membership in Original Set

Informal description

For a finite set $s$ of natural numbers and a natural number $n$ such that every element $m \in s$ satisfies $m < n$, an element $a$ of $\text{Fin}\ n$ belongs to the finite set $\text{attachFin}\ s\ h$ if and only if the corresponding natural number $(a : \mathbb{N})$ belongs to $s$.

Finset.coe_attachFin theorem

{s : Finset ℕ} (h : ∀ m ∈ s, m < n) : (attachFin s h : Set (Fin n)) = Fin.val ⁻¹' s

Full source

@[simp]
lemma coe_attachFin {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :
    (attachFin s h : Set (Fin n)) = Fin.valFin.val ⁻¹' s := by
  ext; simp

Preimage Characterization of $\text{attachFin}$

Informal description

Given a finite set $s$ of natural numbers and a natural number $n$ such that every element $m \in s$ satisfies $m < n$, the underlying set of $\text{attachFin}\ s\ h$ (viewed as a subset of $\text{Fin}\ n$) is equal to the preimage of $s$ under the canonical embedding $\text{Fin}\ n \to \mathbb{N}$.

Finset.card_attachFin theorem

(s : Finset ℕ) (h : ∀ m ∈ s, m < n) : (s.attachFin h).card = s.card

Full source

@[simp]
theorem card_attachFin (s : Finset ℕ) (h : ∀ m ∈ s, m < n) :
    (s.attachFin h).card = s.card :=
  Multiset.card_pmap _ _ _

Cardinality Preservation under $\text{attachFin}$

Informal description

For any finite set $s$ of natural numbers and a natural number $n$, if every element $m \in s$ satisfies $m < n$, then the cardinality of the finite set $\text{attachFin}\ s\ h$ (which consists of the corresponding elements of $\text{Fin}\ n$) is equal to the cardinality of $s$. That is, $|\text{attachFin}\ s\ h| = |s|$.

Finset.image_val_attachFin theorem

{s : Finset ℕ} (h : ∀ m ∈ s, m < n) : image Fin.val (s.attachFin h) = s

Full source

@[simp]
lemma image_val_attachFin {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :
    image Fin.val (s.attachFin h) = s := by
  apply coe_injective
  rw [coe_image, coe_attachFin, Set.image_preimage_eq_iff]
  exact fun m hm ↦ ⟨⟨m, h m hm⟩, rfl⟩

Image of $\text{attachFin}$ under Value Function Equals Original Set

Informal description

For any finite set $s$ of natural numbers and a natural number $n$ such that every element $m \in s$ satisfies $m < n$, the image of the finite set $\text{attachFin}\ s\ h$ (viewed as a subset of $\text{Fin}\ n$) under the canonical embedding $\text{Fin}\ n \to \mathbb{N}$ is equal to $s$. In other words, applying the value function to each element of $\text{attachFin}\ s\ h$ recovers the original set $s$.

Finset.map_valEmbedding_attachFin theorem

{s : Finset ℕ} (h : ∀ m ∈ s, m < n) : map Fin.valEmbedding (s.attachFin h) = s

Full source

@[simp]
lemma map_valEmbedding_attachFin {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :
    map Fin.valEmbedding (s.attachFin h) = s := by
  simp [map_eq_image]

Image of $\text{attachFin}$ under Value Embedding Equals Original Set

Informal description

For any finite set $s$ of natural numbers and a natural number $n$ such that every element $m \in s$ satisfies $m < n$, the image of the finite set $\text{attachFin}\ s\ h$ (viewed as a subset of $\text{Fin}\ n$) under the canonical embedding $\text{Fin}\ n \hookrightarrow \mathbb{N}$ is equal to $s$. In other words, applying the value function to each element of $\text{attachFin}\ s\ h$ recovers the original set $s$.

Finset.attachFin_subset_attachFin_iff theorem

{s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n) : s.attachFin hs ⊆ t.attachFin ht ↔ s ⊆ t

Full source

@[simp]
lemma attachFin_subset_attachFin_iff {s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n) :
    s.attachFin hs ⊆ t.attachFin hts.attachFin hs ⊆ t.attachFin ht ↔ s ⊆ t := by
  simp [← map_subset_map (f := Fin.valEmbedding)]

Subset Equivalence for Finite Sets in $\text{Fin}\ n$: $\text{attachFin}\ s\ hs \subseteq \text{attachFin}\ t\ ht \leftrightarrow s \subseteq t$

Informal description

Let $s$ and $t$ be finite sets of natural numbers such that every element $m \in s$ satisfies $m < n$ and every element $m \in t$ satisfies $m < n$. Then the finite set $\text{attachFin}\ s\ hs$ is a subset of $\text{attachFin}\ t\ ht$ if and only if $s$ is a subset of $t$.

Finset.attachFin_subset_attachFin theorem

 {s t : Finset ℕ} (hst : s ⊆ t) (ht : ∀ m ∈ t, m < n) : s.attachFin (fun m hm ↦ ht m (hst hm)) ⊆ t.attachFin ht

Full source

@[mono, gcongr]
lemma attachFin_subset_attachFin {s t : Finset ℕ} (hst : s ⊆ t) (ht : ∀ m ∈ t, m < n) :
    s.attachFin (fun m hm ↦ ht m (hst hm)) ⊆ t.attachFin ht := by simpa

Subset Preservation under $\text{attachFin}$

Informal description

Let $s$ and $t$ be finite sets of natural numbers such that $s \subseteq t$, and suppose every element $m \in t$ satisfies $m < n$. Then the finite set $\text{attachFin}\ s\ h_s$ is a subset of $\text{attachFin}\ t\ h_t$, where $h_s$ is the proof that all elements of $s$ are less than $n$ (derived from $hst$ and $ht$), and $h_t$ is the proof that all elements of $t$ are less than $n$.

Finset.attachFin_ssubset_attachFin_iff theorem

{s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n) : s.attachFin hs ⊂ t.attachFin ht ↔ s ⊂ t

Full source

@[simp]
lemma attachFin_ssubset_attachFin_iff {s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n) :
    s.attachFin hs ⊂ t.attachFin hts.attachFin hs ⊂ t.attachFin ht ↔ s ⊂ t := by
  simp [← map_ssubset_map (f := Fin.valEmbedding)]

Strict Subset Equivalence under $\mathrm{attachFin}$

Informal description

Let $s$ and $t$ be finite sets of natural numbers such that every element $m \in s$ satisfies $m < n$ and every element $m \in t$ satisfies $m < n$. Then the finite set $\mathrm{attachFin}\,s\,hs$ is a strict subset of $\mathrm{attachFin}\,t\,ht$ if and only if $s$ is a strict subset of $t$. In other words: $$ \mathrm{attachFin}\,s\,hs \subset \mathrm{attachFin}\,t\,ht \leftrightarrow s \subset t. $$

Finset.attachFin_ssubset_attachFin theorem

 {s t : Finset ℕ} (hst : s ⊂ t) (ht : ∀ m ∈ t, m < n) : s.attachFin (fun m hm ↦ ht m (hst.subset hm)) ⊂ t.attachFin ht

Full source

@[mono, gcongr]
lemma attachFin_ssubset_attachFin {s t : Finset ℕ} (hst : s ⊂ t) (ht : ∀ m ∈ t, m < n) :
    s.attachFin (fun m hm ↦ ht m (hst.subset hm)) ⊂ t.attachFin ht := by simpa

Strict Subset Preservation under $\text{attachFin}$

Informal description

Let $s$ and $t$ be finite sets of natural numbers such that $s$ is a strict subset of $t$ (i.e., $s \subset t$), and suppose every element $m \in t$ satisfies $m < n$. Then the finite set $\text{attachFin}\ s\ h_s$ is a strict subset of $\text{attachFin}\ t\ h_t$, where $h_s$ is the proof that all elements of $s$ are less than $n$ (derived from $hst$ and $ht$), and $h_t$ is the proof that all elements of $t$ are less than $n$.

Finset.fin definition

(n : ℕ) (s : Finset ℕ) : Finset (Fin n)

Full source

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

This definition was introduced to define a `LocallyFiniteOrder` instance on `Fin n`.
Later, this instance was rewritten using a more efficient `attachFin`.
Since this definition had no other uses in the library, it was deprecated.
-/
@[deprecated attachFin (since := "2025-04-08")]
protected def fin (n : ℕ) (s : Finset ℕ) : Finset (Fin n) :=
  (s.subtype _).map Fin.equivSubtype.symm.toEmbedding

Finite set of `Fin n` elements from natural number set

Informal description

Given a natural number $n$ and a finite set $s$ of natural numbers, the operation `Finset.fin n s` constructs a finite set of elements in `Fin n` (the canonical type with $n$ elements) by first taking the subset of $s$ consisting of elements less than $n$ (with their membership proofs), then mapping these elements to `Fin n` via the inverse of the natural equivalence between `Fin n` and natural numbers less than $n$. More precisely, this is equivalent to $\{a \in \text{Fin } n \mid a \in s\}$, where $a$ is considered as a natural number via the canonical coercion.

Finset.mem_fin theorem

{s : Finset ℕ} : ∀ a : Fin n, a ∈ s.fin n ↔ (a : ℕ) ∈ s

Full source

@[simp, deprecated mem_attachFin (since := "2025-04-08")]
theorem mem_fin {s : Finset ℕ} : ∀ a : Fin n, a ∈ s.fin na ∈ s.fin n ↔ (a : ℕ) ∈ s
  | ⟨a, ha⟩ => by simp [Finset.fin, ha, and_comm]

Membership in `Finset.fin` via Natural Number Coercion

Informal description

For any finite set $s$ of natural numbers and any element $a$ of the type `Fin n` (natural numbers less than $n$), the element $a$ belongs to the finite set `s.fin n` if and only if the underlying natural number of $a$ (via the canonical coercion) belongs to $s$.

Finset.coe_fin theorem

(n : ℕ) (s : Finset ℕ) : (s.fin n : Set (Fin n)) = Fin.val ⁻¹' s

Full source

@[simp, deprecated coe_attachFin (since := "2025-04-08")]
theorem coe_fin (n : ℕ) (s : Finset ℕ) : (s.fin n : Set (Fin n)) = Fin.valFin.val ⁻¹' s := by ext; simp

Equality between `fin` construction and preimage under canonical embedding

Informal description

For any natural number $n$ and finite set $s$ of natural numbers, the underlying set of the finite set `s.fin n` (which consists of elements of `Fin n` corresponding to elements of $s$ less than $n$) is equal to the preimage of $s$ under the canonical embedding `Fin.val : Fin n → ℕ`. In other words, $\{x \in \text{Fin } n \mid x \in s.\text{fin } n\} = \{x \in \text{Fin } n \mid x \in s\}$, where $x$ is interpreted as a natural number via the canonical embedding.

Finset.fin_mono theorem

: Monotone (Finset.fin n)

Full source

@[mono, deprecated attachFin_subset_attachFin (since := "2025-04-08")]
theorem fin_mono : Monotone (Finset.fin n) := fun s t h x => by simpa using @h x

Monotonicity of `Finset.fin n` with respect to subset inclusion

Informal description

The function `Finset.fin n`, which maps a finite set of natural numbers to a finite set of elements in `Fin n`, is monotone with respect to the subset relation. That is, for any two finite sets of natural numbers $s$ and $t$, if $s \subseteq t$, then $s.\text{fin} n \subseteq t.\text{fin} n$.

Finset.fin_subset_fin theorem

(n : ℕ) {s t : Finset ℕ} (h : s ⊆ t) : s.fin n ⊆ t.fin n

Full source

@[gcongr, deprecated attachFin_subset_attachFin (since := "2025-04-08")]
theorem fin_subset_fin (n : ℕ) {s t : Finset ℕ} (h : s ⊆ t) : s.fin n ⊆ t.fin n := fin_mono h

Subset Preservation under `fin` Construction: $s \subseteq t \implies s.\text{fin}\,n \subseteq t.\text{fin}\,n$

Informal description

For any natural number $n$ and finite sets $s, t$ of natural numbers, if $s \subseteq t$, then the finite set $s.\text{fin}\,n \subseteq t.\text{fin}\,n$ in $\text{Fin}\,n$.

Finset.fin_map theorem

{s : Finset ℕ} : (s.fin n).map Fin.valEmbedding = s.filter (· < n)

Full source

@[simp, deprecated map_valEmbedding_attachFin (since := "2025-04-08")]
theorem fin_map {s : Finset ℕ} : (s.fin n).map Fin.valEmbedding = s.filter (· < n) := by
  simp [Finset.fin, Finset.map_map]

Image of Finite Set under Natural Embedding Equals Filtered Set: $\text{map}(\text{valEmbedding})(\text{fin}_n(s)) = s \text{.filter } (x < n)$

Informal description

For any finite set $s$ of natural numbers, the image of the finite set $\text{fin}_n(s)$ (consisting of elements of $s$ interpreted as elements of $\text{Fin}\,n$) under the natural embedding $\text{Fin}\,n \hookrightarrow \mathbb{N}$ is equal to the subset of $s$ containing elements less than $n$, i.e., $$ \text{map}(\text{valEmbedding})(\text{fin}_n(s)) = \{x \in s \mid x < n\}. $$

Finset.attachFin_eq_fin theorem

{s : Finset ℕ} (h : ∀ m ∈ s, m < n) : attachFin s h = s.fin n

Full source

@[deprecated "No replacement" (since := "2025-04-08")]
theorem attachFin_eq_fin {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :
    attachFin s h = s.fin n := by
  ext
  simp

Equality of Finite Set Constructions in $\text{Fin}\ n$

Informal description

For any finite set $s$ of natural numbers and a natural number $n$, if every element $m \in s$ satisfies $m < n$, then the finite set $\text{attachFin}\ s\ h$ of elements in $\text{Fin}\ n$ is equal to the finite set $s.\text{fin}\ n$.

Main declarations