Coordinate slices through a point of an open set stay in the set nearby

Let $n$ be a natural number, $V\subseteq\mathbb R^n$ an open set, $x\in V$ and $i$ a coordinate index. Then for all $u$ in some neighbourhood of $x_i$ the point $x[x_i:=u]$ (the point $x$ with its $i$-th coordinate replaced by $u$) lies in $V$:

(Stated as an eventually-true property in the neighbourhood filter of $x_i$; $n=0$ is allowed and vacuous.)

Locality lemma: on an open domain, facts about a coordinate slice may be used only near the current coordinate value; it is what lets the certificates transfer differentiability from the domain to each one-variable slice.

Formalization Note Points are functions $\mathrm{Fin}\,n\to\mathbb R$ with the product topology; the conclusion is ∀ᶠ u in 𝓝 (x i), Function.update x i u ∈ V.