Encodable and Denumerable instances for Finset

@[implicit_reducible]

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

If α is encodable, then so is Finset α.

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

The elements of a Fintype as a sorted list.

@[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.

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, ...].

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.

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

theorem Denumerable.raise_lower' {l : List ℕ} {n : ℕ} : (∀ m ∈ l, n ≤ m) → l.SortedLT → raise' (lower' l n) n = l

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

theorem Denumerable.isChain_cons_raise' (l : List ℕ) (m : ℕ) : List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) (m :: raise' l (m + 1))

theorem Denumerable.isChain_cons_raise'_of_lt (l : List ℕ) {m n : ℕ} (h : m < n) : List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) (m :: raise' l n)

theorem Denumerable.raise'_sorted (l : List ℕ) (n : ℕ) : (raise' l n).SortedLT

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.

@[implicit_reducible]

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.