Menger and sigma-compact properties of ordinal Vietoris powers

For a countable ordinal α with ω<α<ω₁, consider Almeida’s compact-range Vietoris power K(α,ord), equipped with the range-plus-finite-coordinate topology. Is it second countable and Lindelöf but neither σ-compact nor Menger?

Why it matters and what counts as progress

Why it matters: This distinguishes countable covering properties that need not persist in these hyperspace constructions.

What counts as progress: A proof for the entire countable-ordinal interval, extending the known ω+1 case, or an ordinal violating one of the stated properties.

How the problem developed

2026 · Theorem [1]
Luis Almeida, with ChatGPT Astra credited for the main argument and Lean formalization Reported that the Vietoris space of nonempty closed subsets of each countable ordinal above ω is second countable and Lindelöf, but neither σ-compact nor Menger.

AI contribution

Astra-led proof extends a Vietoris obstruction to countable ordinals

For every ordinal ω<α<ω₁, Almeida’s compact-range Vietoris power K(α,ord), with its range-plus-finite-coordinate topology, is second-countable and Lindelöf but neither σ-compact nor Menger. The Lean theorem ordinal_full covers this interval by a delayed diagonal.

AI involvementAI-centered

ImportanceNotable

Technical verificationFormal (Lean 4.19.0)

Human understandingFull