This file contains a helper function that generates all possible lists over a given list of candidates such that each of the lists has a given length. Since the definition would hardly be useful in proofs, the accompanying theorem states the desired properties ensured by the definition.

def all_lists_of_length {α : Type u_1} (candidates : List α) : Nat → List (List α)

Equations

• all_lists_of_length candidates Nat.zero = [[]]
• all_lists_of_length candidates n.succ = List.flatMap (fun (t : α) => List.map (fun (ts : List α) => t :: ts) (all_lists_of_length candidates n)) candidates

theorem mem_all_lists_of_length {α : Type u_1} (candidates : List α) (length : Nat) (as : List α) : as ∈ all_lists_of_length candidates length ↔ as.length = length ∧ ∀ (a : α), a ∈ as → a ∈ candidates