Encodable and Denumerable instances for Finset

instance Finset.encodable {α : Type u_1} [Encodable α] : Encodable (Finset α)

If α is encodable, then so is Finset α.

Equations

• One or more equations did not get rendered due to their size.

def Encodable.sortedUniv (α : Type u_1) [Fintype α] [Encodable α] : List α

The elements of a Fintype as a sorted list.

Equations

• Encodable.sortedUniv α = Finset.sort (⇑(Encodable.encode' α) ⁻¹'o fun (x1 x2 : ℕ) => x1 ≤ x2) Finset.univ

@[simp]

theorem Encodable.mem_sortedUniv {α : Type u_1} [Fintype α] [Encodable α] (x : α) : x ∈ sortedUniv α

@[simp]

theorem Encodable.length_sortedUniv (α : Type u_1) [Fintype α] [Encodable α] : (sortedUniv α).length = Fintype.card α

@[simp]

theorem Encodable.sortedUniv_nodup (α : Type u_1) [Fintype α] [Encodable α] : (sortedUniv α).Nodup

@[simp]

theorem Encodable.sortedUniv_toFinset (α : Type u_1) [Fintype α] [Encodable α] [DecidableEq α] : (sortedUniv α).toFinset = Finset.univ

def Encodable.fintypeEquivFin {α : Type u_1} [Fintype α] [Encodable α] : α ≃ Fin (Fintype.card α)

An encodable Fintype is equivalent to the same size Fin.

Equations

• Encodable.fintypeEquivFin = (List.Nodup.getEquivOfForallMemList (Encodable.sortedUniv α) ⋯ ⋯).symm.trans (Equiv.cast ⋯)

def Denumerable.lower' : List ℕ → ℕ → List ℕ

Outputs the list of differences minus one of the input list, that is lower' [a₁, a₂, a₃, ...] n = [a₁ - n, a₂ - a₁ - 1, a₃ - a₂ - 1, ...].

Equations

• Denumerable.lower' [] x✝ = []
• Denumerable.lower' (m :: l) x✝ = (m - x✝) :: Denumerable.lower' l (m + 1)

def Denumerable.raise' : List ℕ → ℕ → List ℕ

Outputs the list of partial sums plus one of the input list, that is raise [a₁, a₂, a₃, ...] n = [n + a₁, n + a₁ + a₂ + 1, n + a₁ + a₂ + a₃ + 2, ...]. Adding one each time ensures the elements are distinct.

Equations

• Denumerable.raise' [] x✝ = []
• Denumerable.raise' (m :: l) x✝ = (m + x✝) :: Denumerable.raise' l (m + x✝ + 1)

theorem Denumerable.lower_raise' (l : List ℕ) (n : ℕ) : lower' (raise' l n) n = l

theorem Denumerable.raise_lower' {l : List ℕ} {n : ℕ} : (∀ m ∈ l, n ≤ m) → List.Sorted (fun (x1 x2 : ℕ) => x1 < x2) l → raise' (lower' l n) n = l

theorem Denumerable.raise'_chain (l : List ℕ) {m n : ℕ} : m < n → List.Chain (fun (x1 x2 : ℕ) => x1 < x2) m (raise' l n)

theorem Denumerable.raise'_sorted (l : List ℕ) (n : ℕ) : List.Sorted (fun (x1 x2 : ℕ) => x1 < x2) (raise' l n)

raise' l n is a strictly increasing sequence.

def Denumerable.raise'Finset (l : List ℕ) (n : ℕ) : Finset ℕ

Makes raise' l n into a finset. Elements are distinct thanks to raise'_sorted.

Equations

• Denumerable.raise'Finset l n = { val := ↑(Denumerable.raise' l n), nodup := ⋯ }

instance Denumerable.finset {α : Type u_1} [Denumerable α] : Denumerable (Finset α)

If α is denumerable, then so is Finset α. Warning: this is not the same encoding as used in Finset.encodable.

Equations

• One or more equations did not get rendered due to their size.