I am looking for a version of [Ehresmann's theorem](https://en.wikipedia.org/wiki/Ehresmann%27s_lemma) for analytic manifolds over the $p$-adic numbers $\mathbb{Q}\_p$ or, more generally, local fields. I follow the conventions from Serre's book "Lie algebras and Lie groups" concerning analytic manifolds over local fields.


Recall that Ehresmann's theorem states that a proper submersion between smooth manifolds is a locally trivial fibration.



> 
> Does a version of this hold for analytic manifolds over $\mathbb{Q}\_p$? Namely, is a proper submersion between analytic manifolds over $\mathbb{Q}\_p$ a locally trivial fibration?
> 
> 
> 



Ehresmann's theorem over the $p$-adics
It seems to me that the following lines essentially show that the answer is yes. Let $f\colon X\to Y$ be a proper submersion of $p$-adic manifolds, we want to show that $f$ is locally trivial on the target:
every point $y$ has an open neighborhood $V$ such that $f\_V\colon f^{-1}(V)\to V$ is isomorphic to the projection $p\_2\colon U\times V\to V$
of a product.


By the inverse function theorem, $f$ is locally trivial on the source:
for every point $x\in X$, there exists an open neighborhood $W$ of $x$
such that $f|\_W\colon W\to f(W)$ is isomorphic to a product.


Let $y\in Y$ and let us cover the compact manifold $f^{-1}(y)$ by a finite family $(W\_i)$ of open subsets 
on which $f$ is isomorphic to a product $U\_i\times V\_i \to V\_i$. 
Let us refine it to a *disjoint* finite covering, still denoted by the same letter, of the same form.
The union $W=\bigcup W\_i$ is an open neighborhood of $f^{-1}(y)$.
Since $f$ is proper, there exists an open neighborhood $V$ of $y$ such that $W$ contains $f^{-1}(V)$. Replacing $V\_i$ by $V$, we are reduced to the case $V\_i=V$ for all $i$.
It is now visible that $f^{-1}(V)$ is isomorphic to the projection
of the product $U\times V\to V$, where $U$ is defined as the disjoint union of the $U\_i$.


