Finsets of prefixes and suffixes

For a finite set S of lists, Finset.prefixes S is the finite set of all prefixes of elements of S, and Finset.suffixes S the finite set of all suffixes of elements of S. The two operations have dual APIs: membership characterizations (mem_prefixes/mem_suffixes), self-membership, and closure under taking further prefixes/suffixes.

This file lives in Complexitylib/Mathlib/ because it extends a Mathlib type in its home namespace — the sanctioned exception to the Complexity root-namespace rule. Its contents are candidates for upstreaming to Mathlib.

def Finset.prefixes {α : Type u_1} [DecidableEq α] (S : Finset (List α)) : Finset (List α)

The finite set of all prefixes of elements of S.

Equations

• S.prefixes = S.biUnion fun (s : List α) => s.inits.toFinset

def Finset.suffixes {α : Type u_1} [DecidableEq α] (S : Finset (List α)) : Finset (List α)

The finite set of all suffixes of elements of S.

Equations

• S.suffixes = S.biUnion fun (s : List α) => s.tails.toFinset

theorem Finset.mem_prefixes {α : Type u_1} [DecidableEq α] {S : Finset (List α)} {p : List α} : p ∈ S.prefixes ↔ ∃ s ∈ S, p <+: s

theorem Finset.mem_suffixes {α : Type u_1} [DecidableEq α] {S : Finset (List α)} {w : List α} : w ∈ S.suffixes ↔ ∃ s ∈ S, w <:+ s

theorem Finset.mem_prefixes_self {α : Type u_1} [DecidableEq α] {S : Finset (List α)} {s : List α} (hs : s ∈ S) : s ∈ S.prefixes

theorem Finset.mem_suffixes_self {α : Type u_1} [DecidableEq α] {S : Finset (List α)} {s : List α} (hs : s ∈ S) : s ∈ S.suffixes

theorem Finset.nil_mem_prefixes {α : Type u_1} [DecidableEq α] {S : Finset (List α)} (hS : S.Nonempty) : [] ∈ S.prefixes

theorem Finset.nil_mem_suffixes {α : Type u_1} [DecidableEq α] {S : Finset (List α)} (hS : S.Nonempty) : [] ∈ S.suffixes

theorem Finset.mem_prefixes_of_prefix {α : Type u_1} [DecidableEq α] {S : Finset (List α)} {p q : List α} (hpq : p <+: q) (hq : q ∈ S.prefixes) : p ∈ S.prefixes

S.prefixes is downward closed under taking prefixes.

theorem Finset.mem_suffixes_of_suffix {α : Type u_1} [DecidableEq α] {S : Finset (List α)} {w v : List α} (hwv : w <:+ v) (hv : v ∈ S.suffixes) : w ∈ S.suffixes

S.suffixes is downward closed under taking suffixes.