Finsets in `Fin n` #

A few constructions for Finsets in Fin n.

Main declarations #

Finset.attachFin: Turns a Finset of naturals strictly less than n into a Finset (Fin n).

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

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.

Equations

s.attachFin h = { val := Multiset.pmap (fun (a : ℕ) (ha : a < n) => ⟨a, ha⟩) s.val h, nodup := ⋯ }

source

@[simp]

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

a ∈ s.attachFin h ↔ ↑a ∈ s

source

@[simp]

theorem Finset.coe_attachFin {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :

↑(s.attachFin h) = Fin.val ⁻¹' ↑s

source

@[simp]

theorem Finset.card_attachFin {n : ℕ} (s : Finset ℕ) (h : ∀ m ∈ s, m < n) :

(s.attachFin h).card = s.card

source

@[simp]

theorem Finset.image_val_attachFin {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :

image Fin.val (s.attachFin h) = s

source

@[simp]

theorem Finset.map_valEmbedding_attachFin {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :

map Fin.valEmbedding (s.attachFin h) = s

source

@[simp]

theorem Finset.attachFin_subset_attachFin_iff {n : ℕ} {s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n) :

s.attachFin hs ⊆ t.attachFin ht ↔ s ⊆ t

source

theorem Finset.attachFin_subset_attachFin {n : ℕ} {s t : Finset ℕ} (hst : s ⊆ t) (ht : ∀ m ∈ t, m < n) :

s.attachFin ⋯ ⊆ t.attachFin ht

source

@[simp]

theorem Finset.attachFin_ssubset_attachFin_iff {n : ℕ} {s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n) :

s.attachFin hs ⊂ t.attachFin ht ↔ s ⊂ t

source

theorem Finset.attachFin_ssubset_attachFin {n : ℕ} {s t : Finset ℕ} (hst : s ⊂ t) (ht : ∀ m ∈ t, m < n) :

s.attachFin ⋯ ⊂ t.attachFin ht

source

@[deprecated Finset.attachFin (since := "2025-04-08")]

def Finset.fin (n : ℕ) (s : Finset ℕ) :

Finset (Fin n)

Given a finset s of natural numbers and a bound n, s.fin n is the finset of all elements of s less than n.

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.

Equations