Let $G$ be a non discrete Polish group. Let $K$ be a compact set of $G$, $C$ a closed set of $G^n$ and $B$ an open set of $G^n$. Suppose $K^n\cap C\subseteq B$. Prove that there is an open set of $G$, say $U$, such that $K\subseteq U$ and $U^n\cap C\subseteq B$.
Geometrically, I think it is quite clear but I can't prove it formally. It is clear that also $K^n\cap C$ is a compact of $G^n$. Maybe we need only that $G$ is an Hausdorff space but I'm not sure. Thank you very much.
Let $d$ be a metric inducing the topology of $G$ and endow $G^n$ with the metric
$$d_{\infty}(x,y) = \max \,\{ d(x_k,y_k) : 1 \leqslant k \leqslant n\}.$$
Then $d_{\infty}$ induces the product topology on $G^n$ (see (1)).
Since $K^n \cap C$ is a compact subset of $B$, there is an $r > 0$ such that $B_{r}^{d_{\infty}}(K^n\cap C) \subseteq B$ (see (2)). The set
$$C_r = C \setminus B_r^{d_{\infty}}(K^n \cap C)$$
is closed and disjoint from $K^n$, so there is a $\rho > 0$ with $B_\rho^{d_{\infty}}(K^n) \cap C_r = \varnothing$ (see also (2)).
Choose $\varepsilon \in (0, \min \{r,\rho\})$, and set $U = B_{\varepsilon}^d(K)$. Then $U^n = B_{\varepsilon}^{d_{\infty}}(K^n)$, so $U^n \cap C_r = \varnothing$, hence
$$x \in U^n \cap C \implies x \in B_r^{d_{\infty}}(K^n \cap C) \implies x \in B.$$
(1) The open $d_{\infty}$-ball $B_r^{d_{\infty}}(x) = \{ y : d_{\infty}(x,y) < r\}$ is the product of the open $d$-balls of the same radius around the components of $x$,
$$B_r^{d_{\infty}}(x) = \prod_{k = 1}^n B_r^d(x_k),$$
so it is open in the product topology, and hence the topology induced by $d_{\infty}$ is at most as fine as the product topology. Conversely, if $U$ is open in the product topology, and $x\in U$, then for every $k$ there is an $r_k(x) > 0$ such that $$\prod_{k = 1}^n B^d_{r_k(x)}(x_k) \subseteq U.$$ Then $r(x) = \min \,\{ r_k(x) : 1 \leqslant k \leqslant n\} > 0$, and
$$B_{r(x)}^{d_{\infty}}(x) = \prod_{k = 1}^n B_{r(x)}^d(x_k) \subseteq \prod_{k = 1}^n B^d_{r_k(x)}(x_k) \subseteq U,$$
so $U = \bigcup\limits_{x\in U} B_{r(x)}^{d_{\infty}}(x)$ is also open in the topology induced by $d_{\infty}$, i.e. the topology induced by $d_{\infty}$ is at least as fine as the product topology.
(2) Let $(X,d)$ be a metric space. For $x\in X$ and a subset $A\subseteq X$, we define
$$\operatorname{dist}(x,A) = \inf \,\{ d(x,a) : a \in A\}.$$
Note that $\operatorname{dist}(x,\varnothing) = +\infty$ for all $x\in X$, but $\operatorname{dist}(x,A) < +\infty$ if $A\neq \varnothing$, and for $r \in (0,+\infty)$ we have $$r > \operatorname{dist}(x,A) \iff B_r(x) \cap A \neq \varnothing.$$
Since $B_r(x) \cap A = \varnothing \iff B_r(x) \cap \overline{A} = \varnothing$, this shows that $\operatorname{dist}(x,A) = \operatorname{dist}(x,\overline{A})$ for all $x\in X$ and $A \subseteq X$. Further note $\operatorname{dist}(x,A) = 0 \iff x \in \overline{A}$.
An important feature of $\operatorname{dist}(\,\cdot\,,A)$ is that these functions are continuous. If $A = \varnothing$, the function is constant, hence continuous. If $A\neq \varnothing$, we have
$$\operatorname{dist}(y,A) \leqslant d(y,a) \leqslant d(y,x) + d(x,a)\tag{1}$$
for every $a\in A$, the first inequality holds by definition of $\operatorname{dist}(y,A)$, and the second by the triangle inequality. Taking the infimum on the right hand side of $(1)$, it follows that
$$\operatorname{dist}(y,A) \leqslant d(y,x) + \operatorname{dist}(x,A).\tag{2}$$
Exchanging the roles of $x$ and $y$, we get
$$\operatorname{dist}(x,A) \leqslant d(x,y) + \operatorname{dist}(y,A),\tag{2'}$$
and the symmetry $d(y,x) = d(x,y)$ then yields
$$\lvert \operatorname{dist}(y,A) - \operatorname{dist}(x,A)\rvert \leqslant d(x,y),\tag{3}$$
which shows that $\operatorname{dist}(\,\cdot\,,A)$ is Lipschitz-continuous with Lipschitz constant $1$ for $A \neq \varnothing$.
For $A\subseteq X$ and $0 < r < +\infty$, we define the open $r$-neighbourhood of $A$ as
$$B_r(A) = \{ x\in X : \operatorname{dist}(x,A) < r\}$$
and note
$$B_r(A) = \{x \in X : B_r(x) \cap A \neq \varnothing\} = \bigcup_{a\in A} B_r(a).$$
The latter shows that $B_r(A)$ is indeed open, and since $B_r(\{x\}) = B_r(x)$ the notations are compatible (although it is of course an abuse of notation to use the same notation for different things).
For two subsets $L,M \subseteq X$, we set
$$\operatorname{dist}(L,M) = \inf\, \{\operatorname{dist}(x,M) : x\in L\} = \inf \, \{ d(x,y) : x \in L, y \in M\}.$$
The second formula shows the symmetry $\operatorname{dist}(L,M) = \operatorname{dist}(M,L)$.
Then for $0 < r < +\infty$ we have
$$B_r(L) \cap M = \varnothing \iff r \leqslant \operatorname{dist}(L,M).$$
For, by definition of $B_r(L)$, we have
\begin{align} && B_r(L) \cap M &= \varnothing\\ &\iff& \bigl(\forall x\in M\bigr)\bigl(\operatorname{dist}(x,L) &\geqslant r\bigr)\\ &\iff& \inf \, \{ \operatorname{dist}(x,L) : x \in M\} &\geqslant r\\ &\iff& \operatorname{dist}(M,L) &\geqslant r. \end{align}
Now we note that if $M$ is compact and $L$ closed with $M \cap L = \varnothing$, then $\operatorname{dist}(M,L) > 0$. If $M = \varnothing$ or $L = \varnothing$, then $\operatorname{dist}(M,L) = +\infty$, so we need only consider nonempty sets. Since $M$ is a nonempty compact set, the continuous function $\operatorname{dist}(\,\cdot\,,L)$ attains its minimum on $M$, i.e. there is an $m_L\in M$ with
$$\operatorname{dist}(m_L,L) = \min \,\{ \operatorname{dist}(x,L) : x \in M\}.$$
Since $L$ is closed and $M\cap L = \varnothing$, we have $\operatorname{dist}(x,L) > 0$ for all $x\in M$, so
$$\operatorname{dist}(M,L) = \operatorname{dist}(m_L,L) > 0.$$
In the above argument, we apply this first for $M = K^n\cap C$ and $L = G^n\setminus B$, noting that $$B_r^{d_{\infty}}(K^n\cap C) \cap (G^n\setminus B) = \varnothing \iff B_r^{d_{\infty}}(K^n\cap C) \subseteq B,$$
and then for $M = K^n$ and $L = C_r$.