Restricting a front to an infinite subset

Given a front F on M and an infinite subset N ⊆ M, the restriction F ↾ N (Front.shrink F N) keeps the elements of F all of whose entries lie in N. When N = M ∘ E is an infinite subset of M (E : ℕ → ℕ strictly monotone), shrink F N is a front on N. This is one of the two operations (with the ray, see Fronts.Ray) needed for the Nash-Williams theorem.

shrink F N is in fact the subfront of F living on N: every subfront arises this way, i.e. if F' ⊆ F is itself a front on N, then F' = shrink F N. (This characterization is not formalized here.)

Main definitions

• Front.shrink F N : the elements of F whose entries lie in range N.

Main results

• Front.shrink_isFront : shrink F (M ∘ E) is a front on M ∘ E.

def Front.shrink (F : Set (List ℕ)) (N : ℕ → ℕ) : Set (List ℕ)

The restriction of F to the infinite subset enumerated by N: the elements of F whose entries all lie in range N.

Equations

• Front.shrink F N = {s : List ℕ | s ∈ F ∧ ∀ x ∈ s, x ∈ Set.range N}

def Front.shrinkOn (F : Set (List ℕ)) (X : Set ℕ) : Set (List ℕ)

The restriction of F to a set X (the survey's F ↾ X): the elements of F whose entries all lie in X. Definitionally shrink F N = shrinkOn F (Set.range N), so the enumeration-based shrink and this set-based restriction agree on X = Set.range N.

Equations

• Front.shrinkOn F X = {s : List ℕ | s ∈ F ∧ ∀ x ∈ s, x ∈ X}

theorem Front.shrink_eq_shrinkOn_range (F : Set (List ℕ)) (N : ℕ → ℕ) : shrink F N = shrinkOn F (Set.range N)

theorem Front.shrink_isFront {F : Set (List ℕ)} {M : ℕ → ℕ} (hF : IsFront F M) {E : ℕ → ℕ} (hE : StrictMono E) : IsFront (shrink F (M ∘ E)) (M ∘ E)

The restriction of a front to an infinite subset is a front on that subset. For a front F on M and the infinite subset N = M ∘ E (E strictly monotone), shrink F N is a front on N.

Restriction: further lemmas

theorem Front.shrink_shrink {F : Set (List ℕ)} {N N' : ℕ → ℕ} (h : Set.range N' ⊆ Set.range N) : shrink (shrink F N) N' = shrink F N'

Restricting twice to nested subsets collapses to the inner restriction.

theorem Front.shrink_powK {M e : ℕ → ℕ} (k : ℕ) : shrink (powK M k) (M ∘ e) = powK (M ∘ e) k

The restriction of the uniform front [M]^k to an infinite subset M ∘ e is the uniform front [M ∘ e]^k on that subset.

theorem Front.tree_shrink_subset {F : Set (List ℕ)} {N : ℕ → ℕ} : tree (shrink F N) ⊆ tree F

The tree of a restriction is contained in the tree of the front.

theorem Front.IsFront.shrink_rank_le {F : Set (List ℕ)} {M : ℕ → ℕ} (hF : IsFront F M) {E : ℕ → ℕ} (hE : StrictMono E) : ⋯.rank ≤ hF.rank

Restriction does not increase rank. The restriction of a front to an infinite subset has rank at most that of the front.