def width {n : ℕ} : List (Fin n) → ℕ

Equations

• width x = x.toFinset.card

theorem width_nil {n : ℕ} : width [] = 0

theorem width_single {n : ℕ} (a : Fin n.succ) : width [a] = 1

theorem width_stay {n : ℕ} (a : Fin n.succ) (x : List (Fin n.succ)) (h : a ∈ x.toFinset) : width (a :: x) = width x

def disjoint_lists {α : Type} [DecidableEq α] (x : List α) (y : List α) : Prop

Equations

• disjoint_lists x y = Disjoint x.toFinset y.toFinset

theorem width_disjoint {n : ℕ} {x : List (Fin n)} {y : List (Fin n)} (h : disjoint_lists x y) : width (x ++ y) = width x + width y

theorem width_comm {n : ℕ} (x : List (Fin n)) (y : List (Fin n)) : width (x ++ y) = width (y ++ x)

theorem width_append {n : ℕ} (x : List (Fin n)) (y : List (Fin n)) : width (x ++ y) ≤ width x + width y