Nash-Williams Fronts

Fronts are families of finite sets of natural numbers which generalize the families [M]^k of subsets of size k ∈ ℕ for infinite subsets M ⊆ ℕ. They enjoy a similar combinatorial property, an infinite Ramsey theorem, which is the main result of this file.

The explicit definition of a front is relative to an infinite set M ⊆ ℕ. A family F of finite subsets of M is a front if it satisfies:

1. (Base) Either F = {∅} or ⋃ F = M.
2. (Incomparability) For all s, t ∈ F, if s ⊑ t then s = t.
3. (Density) For all N ∈ [M]^∞ there exists t ∈ F such that t ⊑ N.

Here s ⊑ t is the initial-segment (prefix) relation.

Encoding (enumeration-first)

Everything is represented through increasing enumerations, so a subset of ℕ is its strictly monotone enumeration and the underlying set is recovered as a range.

• An infinite subset of ℕ is a StrictMono map N : ℕ → ℕ; its set is Set.range N.
• A finite subset is a sorted list s : List ℕ; its set is {x | x ∈ s}.
• IsInit s N says s is the initial segment of the sequence N, i.e. s = [N 0, N 1, …, N (s.length - 1)]. This is ⊑ between (the increasing enumeration of) a finite set and an infinite set.
• ⊑ between two finite sets is plain List.IsPrefix (<+:).
• [M]^∞, the infinite subsets of M, is exactly the subsequences M ∘ g for StrictMono g.

Why increasing lists rather than Finset ℕ

Front elements are finite subsets, but the whole theory — incomparability, density, the tree of prefixes and its rank — is phrased in the initial-segment (prefix) order, not just in terms of membership. List.IsPrefix carries that order natively, with the full Mathlib API (and matching Mathlib.SetTheory.Descriptive.Tree, whose nodes are likewise Lists). A Finset ℕ has no intrinsic order, so an initial-segment relation on finsets would have to be reintroduced by sorting and its API rebuilt from scratch. We therefore encode a finite subset by its strictly increasing enumeration (a sorted List ℕ) and bridge to Finset ℕ only at the boundary with Finset-based (e.g. Ramsey) statements, via Finset.sort / List.toFinset.

theorem List.IsPrefix.head_eq {α : Type u_1} {s t : List α} (h : s <+: t) (hne : s ≠ []) : t.head? = s.head?

A prefix keeps the first entry.

def Front.IsInit (s : List ℕ) (N : ℕ → ℕ) : Prop

IsInit s N : the sorted list s is the initial segment of the increasing enumeration N : ℕ → ℕ, i.e. s = [N 0, N 1, …, N (s.length - 1)]. This is the prefix relation ⊑ between a finite set and an infinite set.

Equations

• Front.IsInit s N = (s = List.map N (List.range s.length))

theorem Front.range_prefix_range {m n : ℕ} (h : m ≤ n) : List.range m <+: List.range n

List.range is monotone for the prefix order.

@[simp]

theorem Front.isInit_nil (N : ℕ → ℕ) : IsInit [] N

theorem Front.isInit_take (N : ℕ → ℕ) (n : ℕ) : IsInit (List.map N (List.range n)) N

The length-n initial segment of N is an initial segment of N.

theorem Front.IsInit.getElem {s : List ℕ} {N : ℕ → ℕ} (hs : IsInit s N) {i : ℕ} (h : i < s.length) : s[i] = N i

The i-th entry of an initial segment of N is N i.

theorem Front.IsInit.head_eq {s : List ℕ} {N : ℕ → ℕ} (hs : IsInit s N) (hne : s ≠ []) : s.head? = some (N 0)

The first entry of a nonempty initial segment of N is N 0.

theorem Front.IsInit.eq_of_length {s t : List ℕ} {N : ℕ → ℕ} (hs : IsInit s N) (ht : IsInit t N) (h : s.length = t.length) : s = t

An initial segment is determined by its length: two initial segments of N of equal length are equal.

theorem Front.IsInit.isPrefix {s t : List ℕ} {N : ℕ → ℕ} (ht : IsInit t N) (h : s <+: t) : IsInit s N

A prefix of an initial segment of N is again an initial segment of N.

theorem Front.IsInit.prefix_or_prefix {s t : List ℕ} {N : ℕ → ℕ} (hs : IsInit s N) (ht : IsInit t N) : s <+: t ∨ t <+: s

Two initial segments of the same sequence are prefix-comparable.

structure Front.IsFront (F : Set (List ℕ)) (M : ℕ → ℕ) : Prop

A front relative to an infinite set M, given by its increasing enumeration M : ℕ → ℕ (a StrictMono map, so range M is infinite). F is a family of finite sets (sorted lists) satisfying Base, Incomparability and Density.

• mono : StrictMono M

  M is the increasing enumeration of an infinite subset of ℕ; in particular range M is infinite. Without this a degenerate M (e.g. constant) would vacuously admit "fronts".

• sorted (s : List ℕ) : s ∈ F → List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) s

  Every element of F is the strictly increasing enumeration of a finite set.

• subM (s : List ℕ) : s ∈ F → ∀ x ∈ s, x ∈ Set.range M

  Every element of F is a subset of M.

• base : F = {[]} ∨ ⋃ s ∈ F, {x : ℕ | x ∈ s} = Set.range M

  Base: F = {∅} or the elements of F cover M.

• incomp (s : List ℕ) : s ∈ F → ∀ t ∈ F, s <+: t → s = t

  Incomparability: F is an antichain for the prefix order.

• dense (g : ℕ → ℕ) : StrictMono g → ∃ t ∈ F, IsInit t (M ∘ g)

  Density: every subsequence M ∘ g of M has an initial segment in F.

The uniform fronts [M]^k

The prototypical fronts: [M]^k is the family of size-k subsets of M, i.e. the strictly increasing lists of length k whose entries lie in M.

def Front.powK (M : ℕ → ℕ) (k : ℕ) : Set (List ℕ)

[M]^k : the strictly increasing lists of length k contained in M.

Equations

• Front.powK M k = {s : List ℕ | s.length = k ∧ List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) s ∧ ∀ x ∈ s, x ∈ Set.range M}

theorem Front.rangeMap_mem_powK {M : ℕ → ℕ} (hM : StrictMono M) {e : ℕ → ℕ} (he : StrictMono e) (k : ℕ) : List.map (M ∘ e) (List.range k) ∈ powK M k

The first k values of M ∘ e forms a size-k subset of M, for e strictly monotone. This is the generic member of [M]^k used to witness Base and Density.

theorem Front.isFront_powK {M : ℕ → ℕ} (hM : StrictMono M) (k : ℕ) : IsFront (powK M k) M

[M]^k the family of subsets of M of size k is a front on M.

The Schreier front

The Schreier front on M consists of the non-empty finite subsets s ⊆ M whose size is one more than the minimal (first) element: ∃ a, s.head? = some a ∧ s.length = a + 1. It is the first genuinely non-uniform front — the lists' length varies with where the list starts.

def Front.schreier (M : ℕ → ℕ) : Set (List ℕ)

The Schreier front on M: increasing lists s ⊆ M whose length is one more than their first element.

Equations

• Front.schreier M = {s : List ℕ | (∃ (a : ℕ), s.head? = some a ∧ s.length = a + 1) ∧ List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) s ∧ ∀ x ∈ s, x ∈ Set.range M}

theorem Front.isFront_schreier {M : ℕ → ℕ} (hM : StrictMono M) : IsFront (schreier M) M

The Schreier front is a front on M.