Polynomial and rational coordinates on locally closed affine neighborhoods

Let $K$ be an algebraically closed field and $\sigma$ a finite set of coordinate indices. Let $I\subseteq K[t_s:s\in\sigma]$ be any ideal, and give $V(I)\subseteq K^\sigma$ its Zariski topology. Let $X$ be a topological space and $d:X\hookrightarrow V(I)$ a topological embedding with locally closed image. For every $x\in X$ and open neighborhood $W$ of $x$, there exist an open subset $S$, a nonnegative integer $n$, a radical ideal $J\subseteq K[u_1,\ldots,u_n]$, and a homeomorphism

with both of the following coordinate properties.

For each original coordinate $s\in\sigma$ there is a polynomial $L_s\in K[u_1,\ldots,u_n]$, fixed throughout $S$, such that

For each new coordinate $i$ there are polynomials $P_i,Q_i\in K[t_s:s\in\sigma]$, fixed throughout $S$, such that

Both affine zero sets have the topology induced by their evaluation-ideal maps into the respective polynomial prime spectra. No radicality assumption is placed on $I$, and neither irreducibility nor smoothness is assumed. The finite coordinate set may be empty, and $n$ may be zero.

Formalization Note. A complete Lean proof constructs the neighborhood by a principal-open refinement of a closed affine subset, followed by adjoining an inverse coordinate with equation $s q-1=0$. It proves the closed-subset presentation, radical graph ideal, inverse maps, both continuity directions in the evaluation-ideal topologies, and reindexing to finitely many numbered variables. The original coordinates are polynomial coordinate functions; every new coordinate is either $t_j/1$ or $1/q$ with nonzero denominator. The proof has no Open theorem dependencies, and the original formal statement and hypotheses are unchanged.