Numerable fiber bundles are hurewicz fibrations

For each nonempty finite word $T=(i_1,\dots ,i_n)$ in $S$, repetitions allowed, put $J_j=[(j-1)\mathrm{/}n,j\mathrm{/}n]$ and ${\lambda }_T(\alpha )={\min }_j{\min }_{v\in J_j}{\rho }_{i_j}(\alpha (v))$. Extrema exist by F6. These functions are continuous on $P$: for a fixed $\alpha$, index all closed interval neighbourhoods on which each relevant original real-valued composite varies by less than $\epsilon \mathrm{/}3$, and take finitely many whose relative interiors cover each $J_j$. Requiring $\beta$ to map each selected compact interval into the inverse image under the relevant ${\rho }_i$ of the $\epsilon \mathrm{/}3$-enlargement of its original value range is a finite compact-open condition. On it the original and new values at every time differ by less than $\epsilon$; minima differ by at most the same bound. Finite minima over $j$ preserve continuity by F5.

Let $V_T=\{\alpha :\alpha (J_j)\subseteq U_{i_j}\text{ for all }j\}$, an open compact-open set. We have $\mathrm{supp}{\lambda }_T\subseteq V_T$. Indeed, outside $V_T$ some $\alpha (v)$ lies outside $U_{i_j}$ and hence outside the closed support of ${\rho }_{i_j}$. The evaluation neighbourhood requiring $\beta (v)$ to remain outside that support is open and makes ${\lambda }_T(\beta )=0$. Thus that $\alpha$ is outside the support. This argument uses neighbourhoods, not sequential convergence.

For each $\alpha$ some ${\lambda }_T(\alpha )>0$. The inverse images of the cozero sets of ${\rho }_i$ cover $I$. Consider all pairs of a centre and a positive radius whose relative interval of twice that radius lies in one cover member. Their smaller intervals cover $I$; choose a finite subcover and a positive minimum of its finitely many radii. Every sufficiently short subinterval lies in one of the corresponding larger intervals: take a point in the short interval, place it in a chosen smaller interval, and use the radius bound on its diameter. Thus a sufficiently fine equal subdivision has every closed $J_j$ contained in one cozero inverse image. Finitely many index choices give a word; each selected continuous positive function has positive minimum on its $J_j$ by F6. Also, for fixed $n$, the family ${\lambda }_T$, $\mathrm{\mid }T\mathrm{\mid }=n$, is locally finite: cover the compact image $\alpha (I)$ by neighbourhoods meeting only finitely many cozero sets of the original partition, extract finitely many, and take their union $O$. The neighbourhood $\{\beta :\beta (I)\subseteq O\}$ meets cozero ${\lambda }_T$ only for words in a fixed finite alphabet, hence only finitely many length-$n$ words. No infinite pointwise choice was made.

Put ${\gamma }_T=\max (0,{\lambda }_T-n{\sum }_{\mathrm{\mid }R\mathrm{\mid }<n}{\lambda }_R)$ for $\mathrm{\mid }T\mathrm{\mid }=n$. The shorter sum is locally finite by step 1.3, hence continuous by F4; F5 proves continuity of ${\gamma }_T$, with $0\le {\gamma }_T\le {\lambda }_T\le 1$. At each $\alpha$, the least length with a positive ${\lambda }_T$ has zero shorter sum, so some ${\gamma }_T(\alpha )>0$. The full family is locally finite: choose $R$ of length $N$ with ${\lambda }_R(\alpha )>0$ and a neighbourhood on which it exceeds $c>0$. For $n>N$ and $nc\ge 1$, every ${\gamma }_T$ of length $n$ vanishes there. Only finitely many lengths remain, each locally finite by step 1.3. Intersect finitely many corresponding neighbourhoods.

For $\alpha \in V_T$ and $0\le s\le t\le 1$, define $L_T(\alpha ,e,s,t)$ by transporting $e$ successively across the intersections of $[s,t]$ with $J_1,\dots ,J_n$. In chart $j$ a segment $[a,b]\subseteq J_j$ sends the current point $z$ to ${\theta }_{i_j}^{-1}(\alpha (b),{\mathrm{pr}}_F{\theta }_{i_j}(z))$; empty segments act identically. After chart $j$ the base point is $\alpha (\min (t,\max (s,j\mathrm{/}n)))$, which proves that the next nonempty segment starts at the current base point. For continuity use the finite closed cases $t\le (j-1)\mathrm{/}n$, $s\ge j\mathrm{/}n$, and $s\le j\mathrm{/}n$, $t\ge (j-1)\mathrm{/}n$. On the third case the segment endpoints are $\max (s,(j-1)\mathrm{/}n)$ and $\min (t,j\mathrm{/}n)$. The other cases use identity. At overlaps the segment has length zero and the chart formula equals identity, so F8 pastes them continuously. F1 and F3 make each nonempty chart formula continuous on its domain, including the incoming point. Iterate finitely many times. In particular $L_T(\alpha ,e,s,s)=e$ exactly.

Set $G={\sum }_T{\gamma }_T>0$ and $w_T={\gamma }_T\mathrm{/}G$. By step 2.1 and F4–F5 these are continuous, locally finite, sum to one, and $\mathrm{supp}{w}_T\subseteq \mathrm{supp}{\lambda }_T\subseteq V_T$. Use AC, precisely through F7, to well-order the set of words. Put $a_T={\sum }_{R<T}{w}_R$ and $b_T=a_T+w_T$; subfamilies are locally finite so these are continuous. At any fixed path the finitely many positive weights, in their induced order, give consecutive intervals $[a_T,b_T]$ filling $[0,1]$.

Given $(e,\alpha )$ with $p(e)=\alpha (0)$ and an endpoint time $t$, process the finitely many positive-weight words in order, applying $L_T$ on $[\min (t,a_T),\min (t,b_T)]$. Consecutive endpoints agree because their untruncated intervals are consecutive, and clipping preserves this. The result $\mathrm{\Lambda }(e,\alpha ,t)$ lies over $\alpha (t)$. At $t=0$ every segment has length zero, so $\mathrm{\Lambda }(e,\alpha ,0)=e$. Inserting zero-weight words changes nothing, by the exact zero-length identity in step 2.2. Thus the definition is independent of any finite list containing all positive weights.

The map $\mathrm{\Lambda }$ is jointly continuous. Near a fixed ${\alpha }_0$, local finiteness leaves only finitely many possibly nonzero weights. For a word in that list with ${\alpha }_0\mathrm{\notin }\mathrm{supp}{w}_T$, shrink the neighbourhood so that its weight vanishes and discard it. For every remaining word, shrink into $V_T$, using the support inclusion in step 3.1. On this single neighbourhood, $\mathrm{\Lambda }$ is a fixed finite composition of the continuous maps in step 2.2 with the continuous clipped endpoint functions. Each formula is defined even when its weight becomes zero, since the whole neighbourhood is in $V_T$. F8 proves joint continuity, including intervals shrinking to length zero and changes of the active list.

For an arbitrary initial map $f:X\to E$ and compatible base homotopy $H:X\times I\to B$, F3 makes $x\mapsto {\alpha }_x=H(x,-)$ continuous. Then $\tilde{H}(x,t)=\mathrm{\Lambda }(f(x),{\alpha }_x,t)$ is continuous by step 5.1, starts at $f(x)$ and projects to $H(x,t)$ by step 4.1. This is the full ordinary HLP of F2. When the bundle spaces and test space are CGWH, their interval cylinders have the ordinary topology, so the same ordinary lift is a lift in that category. This conclusion uses the ordinary charts specified in F1 and asserts nothing about merely k-product charts.

If $B$ is empty then $E$ is empty. If $F$ is empty then again $E$ is empty and only empty initial-map domains occur, so HLP is vacuous. Otherwise the construction covers constant paths, a single active word, zero weights and both endpoints without modification. The well-order in step 3.1 is the sole use of AC; all other selections were finite or a single local witness, and chart assignments were supplied data. Thus the theorem, with its exact choice and topology conventions, is proved.