Higman's Lemma Application for Languages

This file states a consequence of Higman's lemma that is used in the proof of the shrinking lemma for indexed languages.

Main result

higman_finite_antichain: For any set Y of lists over a finite type, the set of minimal elements of Y under the sublist relation is finite.

References

• J. Sakarovitch and I. Simon, "Subwords", in M. Lothaire (ed.), Combinatorics on Words, 1983.
• R. H. Gilman, "A shrinking lemma for indexed languages", Theoret. Comput. Sci. 163 (1996), 277–281.

def minimalElements (α : Type u_1) (Y : Set (List α)) : Set (List α)

The set of minimal elements of a set Y of lists, under the sublist relation. An element x ∈ Y is minimal if no proper sublist of x belongs to Y.

Equations

• minimalElements α Y = {x : List α | x ∈ Y ∧ ∀ y ∈ Y, y.Sublist x → y = x}

theorem higman_finite_antichain (α : Type u_1) [Fintype α] (Y : Set (List α)) : (minimalElements α Y).Finite

theorem exists_minimal_sublist (α : Type u_1) [Fintype α] (Y : Set (List α)) (y : List α) (hy : y ∈ Y) : ∃ x ∈ minimalElements α Y, x.Sublist y