Lexicographically least points of closed subsets of Baire space

Every nonempty closed subset F of the Baire space ℕ → ℕ, and more generally of a product ∀ n, E n of well-ordered spaces, has a least element for the lexicographic order. Its coordinates are chosen one at a time: the n-th coordinate is the least value of the n-th coordinate among the points of F that share its first n coordinates. The points chosen at the successive stages converge to it, so it lies in F because F is closed.

This "leftmost branch" is the canonical choice of a point in a closed subset of Baire space, and it is the choice behind the Jankov–von Neumann uniformization theorem: a set whose points are parametrised continuously by Baire space has a section selecting, over each point of its projection, the image of the lexicographically least parameter. The coordinatewise characterisation TauCeti.isLeast_image_toLex_iff is the form in which that proof consumes it.

The file also records that distinct points of a sequence space eventually have distinct initial segments, uniformly over an injective finite family (PiNat.eventually_injective_res).

Main results

• TauCeti.isLeast_image_toLex_iff: a point β ∈ F is lexicographically least in F exactly when, for every n, its n-th coordinate is the least n-th coordinate among the points of F in the cylinder of its first n coordinates.
• IsClosed.exists_isLeast_image_toLex: a nonempty closed subset of ∀ n, E n, with each E n well-ordered, has a lexicographically least element.
• PiNat.eventually_injective_res: the initial segments of an injective finite family of sequences are pairwise distinct from some length on.

References

• A. S. Kechris, Classical Descriptive Set Theory, Springer-Verlag, 1995, the proof of Theorem 18.1, for the leftmost branch of a closed subset of Baire space.

theorem TauCeti.isLeast_image_toLex_iff {E : ℕ → Type u_1} [(n : ℕ) → LinearOrder (E n)] {F : Set ((n : ℕ) → E n)} {β : (n : ℕ) → E n} (hβ : β ∈ F) : IsLeast (⇑toLex '' F) (toLex β) ↔ ∀ (n : ℕ), IsLeast ((fun (x : (n : ℕ) → E n) => x n) '' (F ∩ PiNat.cylinder β n)) (β n)

A point β of F ⊆ ∀ n, E n is the lexicographically least element of F exactly when, for every n, its n-th coordinate is the least n-th coordinate among the points of F whose first n coordinates agree with those of β.

theorem IsClosed.exists_isLeast_image_toLex {E : ℕ → Type u_1} [(n : ℕ) → LinearOrder (E n)] [∀ (n : ℕ), WellFoundedLT (E n)] [(n : ℕ) → TopologicalSpace (E n)] {F : Set ((n : ℕ) → E n)} (hF : IsClosed F) (hne : F.Nonempty) : ∃ β ∈ F, IsLeast (⇑toLex '' F) (toLex β)

A nonempty closed subset of a product ∀ n, E n of well-ordered spaces, such as the Baire space ℕ → ℕ, has a lexicographically least element.

theorem PiNat.eventually_injective_res {ι : Type u_1} {β : Type u_2} [Finite ι] {a : ι → ℕ → β} (ha : Function.Injective a) : ∀ᶠ (j : ℕ) in Filter.atTop, Function.Injective fun (i : ι) => res (a i) j

Distinct branches of a tree eventually separate: for an injective finite family a of sequences, the initial segments PiNat.res (a i) j of length j are pairwise distinct for all large j.