Encodable and Denumerable instances for Finset

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) → 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.

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.