def List.getElem_prod {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) (i : ℕ) (hi : i < (l₁ ×ˢ l₂).length) : (l₁ ×ˢ l₂)[i] = (l₁[i / l₂.length], l₂[i % l₂.length])

Equations

• ⋯ = ⋯

def Array.product {α : Type u_1} {β : Type u_2} (l₁ : Array α) (l₂ : Array β) : Array (α × β)

Equations

• l₁.product l₂ = Array.flatMap (fun (a : α) => Array.map (Prod.mk a) l₂) l₁

@[implicit_reducible]

instance Array.instSProdProd_weightedNetKAT {α : Type u_1} {β : Type u_2} : SProd (Array α) (Array β) (Array (α × β))

Equations

• Array.instSProdProd_weightedNetKAT = { sprod := Array.product }

theorem Array.product_eq_toList_product {α : Type u_1} {β : Type u_2} (l₁ : Array α) (l₂ : Array β) : (l₁ ×ˢ l₂).toList = l₁.toList ×ˢ l₂.toList

theorem Array.mem_product_iff_mem_toList_product {α : Type u_1} {β : Type u_2} (l₁ : Array α) (l₂ : Array β) {x : α × β} : x ∈ l₁ ×ˢ l₂ ↔ x ∈ l₁.toList ×ˢ l₂.toList

@[simp]

theorem Array.mem_product {α : Type u_1} {β : Type u_2} {l₁ : Array α} {l₂ : Array β} {x : α × β} : x ∈ l₁ ×ˢ l₂ ↔ x.1 ∈ l₁ ∧ x.2 ∈ l₂

@[simp]

theorem Array.mem_product' {α : Type u_1} {β : Type u_2} {l₁ : Array α} {l₂ : Array β} {x : α × β} : x ∈ l₁.product l₂ ↔ x.1 ∈ l₁ ∧ x.2 ∈ l₂

@[simp]

theorem Array.pair_mem_product {α : Type u_1} {β : Type u_2} {l₁ : Array α} {l₂ : Array β} {x : α} {y : β} : (x, y) ∈ l₁ ×ˢ l₂ ↔ x ∈ l₁ ∧ y ∈ l₂

@[simp]

def Array.size_product {α : Type u_1} {β : Type u_2} {l₁ : Array α} {l₂ : Array β} : (l₁ ×ˢ l₂).size = l₁.size * l₂.size

Equations

• ⋯ = ⋯

@[simp]

def Array.getElem_product {α : Type u_1} {β : Type u_2} {l₁ : Array α} {l₂ : Array β} {i : ℕ} (hi : i < (l₁ ×ˢ l₂).size) : (l₁ ×ˢ l₂)[i] = (l₁[i / l₂.size], l₂[i % l₂.size])

Equations

• ⋯ = ⋯

def Array.Nodup {α : Type u_1} (l : Array α) : Prop

Equations

• l.Nodup = Array.Pairwise (fun (x1 x2 : α) => x1 ≠ x2) l

@[simp]

theorem Array.nodup_empty {α : Type u_1} : #[].Nodup

@[simp]

theorem Array.nodup_singleton {α : Type u_1} {a : α} : #[a].Nodup

@[simp]

theorem Array.nodup_pair {α : Type u_1} {a b : α} : #[a, b].Nodup ↔ a ≠ b

theorem Array.nodup_iff_toList_nodup {α : Type u_1} (l : Array α) : l.toList.Nodup ↔ l.Nodup

def Array.Nodup.product {α : Type u_1} {β : Type u_2} {l₁ : Array α} {l₂ : Array β} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) : (l₁ ×ˢ l₂).Nodup

Equations

• ⋯ = ⋯

theorem Array.nodup_append {α : Type u_1} {l₁ l₂ : Array α} : (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, a ≠ b

theorem Array.Nodup.map {α : Type u_1} {β : Type u_2} {l : Array α} {f : α → β} (hf : Function.Injective f) : l.Nodup → (Array.map f l).Nodup

theorem Array.nodup_finRange (n : ℕ) : (Array.finRange n).Nodup

@[simp]

theorem Array.mem_finRange {n : ℕ} (a : Fin n) : a ∈ Array.finRange n

theorem Array.nodup_map_iff_inj_on {α : Type u_1} {β : Type u_2} {f : α → β} {l : Array α} (d : l.Nodup) : (map f l).Nodup ↔ ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y

class Listed (α : Type u_1) : Type u_1

• array : Array α
• nodup : array.Nodup
• size : ℕ
• size_prop : array.size = size α
• complete (a : α) : a ∈ array
• encode : α → ℕ
• encode_len (a : α) : encode a < array.size
• encode_prop (a : α) : array[encode a] = a

@[implicit_reducible]

def Listed.ofArray {α : Type u_1} [DecidableEq α] (array : Array α) (nodup : array.Nodup) (complete : ∀ (a : α), a ∈ array) : Listed α

Equations

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

@[implicit_reducible]

instance Listed.instUnit : Listed Unit

Equations

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

theorem Listed.encode_lt_size {α : Type u_1} [Listed α] (a : α) : encode a < size α

def Listed.encode_inj {α : Type u_1} [Listed α] : Function.Injective encode

Equations

• ⋯ = ⋯

instance Listed.instCountable {α : Type u_1} [Listed α] : Countable α

@[implicit_reducible]

def Listed.lift {α : Type u_1} [Listed α] {γ : Type u_3} (f : α ≃ γ) : Listed γ

Equations

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

@[simp]

theorem Listed.mem_list {α : Type u_1} [Listed α] (a : α) : a ∈ array

def Listed.arrayOf (α : Type u_3) [Listed α] : Array α

Equations

• Listed.arrayOf α = Listed.array

def Listed.listOf (α : Type u_3) [Listed α] : List α

Equations

• Listed.listOf α = Listed.array.toList

@[simp]

theorem Listed.mem_arrayOf {α : Type u_1} [Listed α] (a : α) : a ∈ arrayOf α

@[simp]

theorem Listed.mem_listOf {α : Type u_1} [Listed α] (a : α) : a ∈ listOf α

@[inline, specialize #[]]

def Listed.decode {α : Type u_1} [Listed α] (i : ℕ) : Option α

Equations

• Listed.decode i = Listed.array[i]?

@[simp]

theorem Listed.encode_decode {α : Type u_1} [Listed α] (a : α) : decode (encode a) = some a

theorem Listed.decode_eq_some {α : Type u_1} [Listed α] (n : ℕ) (a : α) : decode n = some a ↔ encode a = n

@[simp]

theorem Listed.decode_get_encode {α : Type u_1} [Listed α] (n : ℕ) (h : (decode n).isSome = true) : encode ((decode n).get h) = n

@[inline, specialize #[]]

def Listed.encodeFin {α : Type u_3} [i : Listed α] : α → Fin (size α)

Equations

• Listed.encodeFin a = ⟨Listed.encode a, ⋯⟩

@[inline, specialize #[]]

def Listed.decodeFin {α : Type u_3} [i : Listed α] : Fin (size α) → α

Equations

• Listed.decodeFin a = (Listed.decode ↑a).get ⋯

@[simp]

theorem Listed.decodeFin_encodeFin {α : Type u_3} [i : Listed α] (a : Fin (size α)) : encodeFin (decodeFin a) = a

@[simp]

theorem Listed.encodeFin_decodeFin {α : Type u_3} [i : Listed α] (a : α) : decodeFin (encodeFin a) = a

def Listed.equivFin {α : Type u_3} [Listed α] : α ≃ Fin (size α)

Equations

• Listed.equivFin = { toFun := Listed.encodeFin, invFun := Listed.decodeFin, left_inv := ⋯, right_inv := ⋯ }

def Listed.decodeFin_inj {α : Type u_1} [Listed α] : Function.Injective decodeFin

Equations

• ⋯ = ⋯

def Listed.encodeFin_bijective {α : Type u_1} [Listed α] : Function.Bijective encodeFin

Equations

• ⋯ = ⋯

def Listed.decodeFin_bijective {α : Type u_1} [Listed α] : Function.Bijective decodeFin

Equations

• ⋯ = ⋯

@[simp]

theorem Listed.encode_eq_iff {α : Type u_3} [Listed α] {a b : α} : encode a = encode b ↔ a = b

@[simp]

theorem Listed.encodeFin_eq_iff {α : Type u_3} [Listed α] {a b : α} : encodeFin a = encodeFin b ↔ a = b

@[simp]

theorem Listed.encodeFin_eq_encode_iff {α : Type u_3} [Listed α] {a b : α} : ↑(encodeFin a) = encode b ↔ a = b

@[simp]

theorem Listed.encode_eq_encodeFin_iff {α : Type u_3} [Listed α] {a b : α} : encode a = ↑(encodeFin b) ↔ a = b

@[implicit_reducible]

def Listed.decidableEq {α : Type u_1} [Listed α] : DecidableEq α

Equations

• Listed.decidableEq a b = if h : Listed.encode a = Listed.encode b then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

def Listed.fintype {α : Type u_1} [Listed α] : Fintype α

Equations

• Listed.fintype = { elems := (Listed.listOf α).toFinset, complete := ⋯ }

@[simp]

theorem Listed.array_toFinset {α : Type u_1} [Listed α] [DecidableEq α] : array.toList.toFinset = Finset.univ

@[implicit_reducible]

instance Listed.instProd {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] : Listed (α × β)

Equations

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

@[implicit_reducible]

instance Listed.instSum {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] : Listed (α ⊕ β)

Equations

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

inductive Listed.T : Type

• a : T
• b : T
• c : T
• d : T

@[implicit_reducible]

instance Listed.instDecidableEqT : DecidableEq T

Equations

• Listed.instDecidableEqT x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Listed.instReprT.repr : T → ℕ → Std.Format

Equations

• Listed.instReprT.repr Listed.T.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Listed.T.a")).group prec✝
• Listed.instReprT.repr Listed.T.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Listed.T.b")).group prec✝
• Listed.instReprT.repr Listed.T.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Listed.T.c")).group prec✝
• Listed.instReprT.repr Listed.T.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Listed.T.d")).group prec✝

@[implicit_reducible]

instance Listed.instReprT : Repr T

Equations

• Listed.instReprT = { reprPrec := Listed.instReprT.repr }

def Listed.instInhabitedT.default : T

Equations

• Listed.instInhabitedT.default = Listed.T.a

@[implicit_reducible]

instance Listed.instInhabitedT : Inhabited T

Equations

• Listed.instInhabitedT = { default := Listed.instInhabitedT.default }

@[implicit_reducible]

instance Listed.instT : Listed T

Equations

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

@[implicit_reducible]

instance Listed.instFin {n : ℕ} : Listed (Fin n)

Equations

• Listed.instFin = { array := Array.finRange n, nodup := ⋯, size := n, size_prop := ⋯, complete := ⋯, encode := fun (a : Fin n) => ↑a, encode_len := ⋯, encode_prop := ⋯ }

@[simp]

theorem Listed.fin_size {n : ℕ} : size (Fin n) = n

@[simp]

theorem Listed.fin_size' {n : ℕ} : array.size = n

@[implicit_reducible]

def Listed.ofEquiv {α : Type u_3} {β : Type u_4} [i : Listed α] (e : α ≃ β) : Listed β

Equations

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

@[simp]

theorem Listed.encode_unit : encode () = 0

@[simp]

theorem Listed.encodeFin_unit : encodeFin () = 0

@[simp]

theorem Listed.size_unit : size Unit = 1

@[simp]

theorem Listed.sum_fin {α : Type u_3} [Listed α] [Fintype α] {𝒮 : Type u_4} [AddCommMonoid 𝒮] {f : Fin (size α) → 𝒮} : ∑ i : Fin (size α), f i = ∑ i : α, f (encodeFin i)

@[implicit_reducible]

instance Listed.instUniqueFinSizeUnit : Unique (Fin (size Unit))

Equations

• Listed.instUniqueFinSizeUnit = { toInhabited := Fin.instInhabited, uniq := Listed.instUniqueFinSizeUnit._proof_5 }

@[simp]

theorem Listed.size_isEmpty {α : Type u_3} [Listed α] [Subsingleton α] [i : IsEmpty α] : size α = 0

@[simp]

theorem Listed.size_subsingleton_nonempty {α : Type u_3} [Listed α] [ss : Subsingleton α] [i : Nonempty α] : size α = 1

@[simp]

theorem Listed.size_unique {α : Type u_3} [Listed α] [i : Unique α] : size α = 1

theorem Listed.size_subsingleton {α : Type u_3} [Listed α] [i : Subsingleton α] : size α ≤ 1

@[simp]

theorem Listed.encodeFin_subsingleton {α : Type u_3} [Listed α] [Subsingleton α] (a : α) : encodeFin a = ⟨0, ⋯⟩

@[simp]

theorem Listed.encode_subsingleton {α : Type u_3} [Listed α] [Subsingleton α] (a : α) : encode a = 0