General helper lemmas

Nothing in this file is about PDL. These are helper definitions and lemmas that are used in several places and might also be in (newer versions of) Mathlib.

Helpers about Lists and Finsets

def List.toFinFin {α : Type u_1} [DecidableEq α] : List (List α) → Finset (Finset α)

Equations

• x✝.toFinFin = (List.map (fun (L : List α) => L.toFinset) x✝).toFinset

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

Turning a mapped list into a Finset is the image of the Finset.

Helpers about List.Vector

theorem List.Vector.tail_last_eq_last {α : Type u_1} {k : ℕ} (l : Vector α k.succ.succ) : l.tail.last = l.last