The Bolzano-Weierstrass Theorem is a very useful result in the theory of metric spaces. It states that given a compact space $X$, a sequence $(u_n) \in X^\omega$ always has a subsequence $(u_{n_k})\in X^\omega$ which is convergent.
Bolzano-Weierstrass can sometimes allow us to make a passage from a theorem being true for a dense subset of cases to being true for all cases. For instance, if we know that every Hermitian matrix that has pairwise distinct eigenvalues can be diagonalised using a unitary matrix, then by appealing to Bolzano-Weierstrass we may conclude that all Hermitian matrices can be diagonalised using unitary matrices. The compactness of the space of unitary matrices is essential here. The need to use compactness (and Bolzano-Weierstrass) stems from the fact that the unitary diagonalisation of a Hermitian matrix does not vary continuously, so we can't take the limit of a sequence, but have to pass to a convergent subsequence.
We know that the manifold $S^n$ (the $n$-sphere) is compact. But its tangent bundle $TS^n$ is not compact. But I'm wondering whether there is a substitute for compactness, and an analogue of the Bolzano-Weierstrass theorem, that we can use for $TS^n$. This might have some connection to formal limits, formal differentiation, Zariski open sets, and other formal analogues of notions from analysis.
