# 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)`.

source
def Finset.attachFin (s : Finset ℕ) {n : ℕ} (h : ∀ m ∈ s, m < n) :
Finset (Fin 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 := ⋯ }

Instances For

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