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

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

Equations

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

def List.productWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : List α) (bs : List β) : List γ

Combine every element of the first list with every element of the second list using the function f.

Equations

• List.productWith f as bs = List.map (fun (x : α × β) => match x with | (a, b) => f a b) (as.product bs)

def List.mulr {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) : List (List α) → List β

Use foldr to combine any element of the first list with any element of the second list, the third list, etc. Note that the size of the result is exponential in the number of lists.

Equations

• List.mulr f init = List.foldr (List.productWith f) [init]

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

@[irreducible]

def List.mergeDedup {α : Type u_1} [Ord α] (xs ys : List α) : List α

Similar to List.merge, but also remove duplicates. I tried to combine List.merge with List.dedup, but there are no lemmas for List.dedup with sorted. There is also Array.mergeDedup, but that also has no lemmas.

Equations

• One or more equations did not get rendered due to their size.
• [].mergeDedup x✝ = x✝
• x✝.mergeDedup [] = x✝

theorem List.mem_mergeDedup {α : Type u_1} [LinearOrder α] {xs ys : List α} {a : α} : a ∈ xs.mergeDedup ys ↔ a ∈ xs ∨ a ∈ ys

theorem List.mergeDedup_sorted {α : Type u_1} [LinearOrder α] {xs ys : List α} : xs.SortedLT → ys.SortedLT → (xs.mergeDedup ys).SortedLT

def List.insertDedup {α : Type u_1} [Ord α] (xs : List α) (x : α) : List α

Equations

• [].insertDedup x✝ = [x✝]
• (x_2 :: xs).insertDedup x✝ = match compare x_2 x✝ with | Ordering.lt => x_2 :: xs.insertDedup x✝ | Ordering.eq => x_2 :: xs | Ordering.gt => x✝ :: x_2 :: xs

theorem List.mem_insertDedup {α : Type u_1} [LinearOrder α] {xs : List α} {x a : α} : a ∈ xs.insertDedup x ↔ a ∈ xs ∨ a = x

theorem List.insertDedup_sorted {α : Type u_1} [LinearOrder α] {xs : List α} {x : α} : xs.SortedLT → (xs.insertDedup x).SortedLT

@[irreducible]

def List.diff' {α : Type u_1} [Ord α] (xs ys : List α) : List α

Equations

• [].diff' x✝ = []
• x✝.diff' [] = x✝
• (x_2 :: xs).diff' (y :: ys) = match compare x_2 y with | Ordering.lt => x_2 :: xs.diff' (y :: ys) | Ordering.eq => xs.diff' ys | Ordering.gt => (x_2 :: xs).diff' ys

theorem List.mem_diff' {α : Type u_1} [LinearOrder α] {xs ys : List α} (h1 : xs.SortedLT) (h2 : ys.SortedLT) (a : α) : a ∈ xs.diff' ys ↔ a ∈ xs ∧ a ∉ ys

theorem List.diff'_sorted {α : Type u_1} [LinearOrder α] {xs ys : List α} : xs.SortedLT → ys.SortedLT → (xs.diff' ys).SortedLT

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