The Vietoris power 
of a topological space 
, with index cardinal number 
, is the set of functions 
with a topological
basis consisting of the sets
![[U;Lambda,V]={f in X^kappa:Im(f) subset= U, f(xi) in V_xi for all xi in Lambda},](/images/equations/VietorisPower/NumberedEquation1.svg) |
where 
and the 
are open sets in 
and 
is a finite set contained
in 
. Thus the topology
combines finitely many coordinate restrictions with the requirement that the entire
range lie in one open set (Caruvana
and Holshouser 2026).
The compact-range Vietoris power is the subspace
 |
The functions in this space need not be continuous or order-preserving. For a countable ordinal number 
, the default index in the notation
is 
.
Almeida (2026a) reported that, for every 
, the space 
is second
countable and therefore Lindelöf, but is neither sigma-compact
nor Menger. The last property means that there is a sequence
of open covers for which no choice of finitely many
members from each cover covers the space. The argument uses a countable topological
basis, a closed copy of 
, and a delayed diagonal construction. ChatGPT
Astra developed the main argument and Lean formalization under Almeida's direction.
An author-directed Codex recheck successfully compiled all eight original Lean modules
and their audit from unchanged sources. The audited declarations used only Lean's
standard logical axioms (Almeida 2026b). As of Oct. 2, 2026, VibeMathed had
not independently rebuilt the development, and independent specialist review had
not been reported (VibeMathed 2026).
to All Countable Ordinals Above 
." 2026.