theorem Array.lt_of_getElem?_eq_some {α : Type u_1} {a : α} {xs : Array α} {i : ℕ} (h : xs[i]? = some a) : i < xs.size

@[simp]

theorem Fintype.elems_eq_univ {α : Type u_1} [h : Fintype α] : elems = Finset.univ

def Vector.elems {α : Type u_1} [h : Fintype α] [DecidableEq α] (n : ℕ) : Finset (Vector α n)

Equations

• Vector.elems 0 = {#v[]}
• Vector.elems n.succ = (Vector.elems n).biUnion fun (v : Vector α n) => Finset.image v.push Fintype.elems

@[implicit_reducible]

instance instFintypeVectorOfDecidableEq_validator {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} : Fintype (Vector α n)

Equations

• instFintypeVectorOfDecidableEq_validator = { elems := Vector.elems n, complete := ⋯ }

theorem Vector.mem_iff_getElem' {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n} : a ∈ xs ↔ ∃ (i : Fin n), xs[i] = a

Variant of Vector.mem_iff_getElem using Fin.

def List.multiply {α : Type u_1} : List (List (List α)) → List (List α)

Equations

• List.multiply = List.mulr✝ (fun (x1 x2 : List α) => x1 ++ x2) []

@[simp]

theorem List.multiply_nil {α : Type u_1} : [].multiply = [[]]

@[simp]

theorem List.multiply_cons {α : Type u_1} {asss : List (List (List α))} {ass : List (List α)} : (ass :: asss).multiply = flatMap (fun (as : List α) => map (fun (x : List α) => as ++ x) asss.multiply) ass

theorem List.map_toFinset {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α → β} {xs : List α} : (map f xs).toFinset = Finset.image f xs.toFinset

theorem List.length_flatten_short {α : Type u_1} (ass : List (List α)) (h : ∀ as ∈ ass, as.length < 2) : ass.flatten.length ≤ ass.length

@[simp]

theorem Set.inter_compl_subset_union_compl {α : Type u_1} {s1 s2 s3 s4 : Set α} : s1 ∩ s2ᶜ ⊆ s3 ∪ s4ᶜ ↔ s1 ∩ s4 ⊆ s3 ∪ s2