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.

noncomputable def Finset.attachList {α : Type u_1} (s : Finset α) : List ↥s

The elements of a finite set, as a list of elements together with membership proofs. This is the Finset analogue of List.attach. It is noncomputable because we have no linear order on the elements, but the order of the list is irrelevant for our purposes.

Equations

• s.attachList = List.map (fun (x : { x : α // x ∈ s.toList }) => ⟨↑x, ⋯⟩) s.toList.attach

@[simp]

theorem Finset.mem_attachList {α : Type u_1} {s : Finset α} (a : ↥s) : a ∈ s.attachList

@[simp]

theorem Finset.attachList_map_val {α : Type u_1} {s : Finset α} : List.map Subtype.val s.attachList = s.toList

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