Joint return lemma for a proximal minimal pair (source code)

= Joint return lemma for a proximal minimal pair

For a compact <metric space> with a <continuous map> $T$, suppose $y$ is a <minimal point> and $x,y$ are <proximal>. Every <neighborhood> $U$ of $y$ admits arbitrarily large $n$ with $T^nx,T^ny\in U$. First shrink $U$ to an open <neighborhood>, then choose an open $V$ with $y\in V$ and $\overline V\subseteq U$. Minimality and <compactness> give a finite cover of the <orbit closure> of $y$ by $T^{-j}V$, $0\leq j\leq J$. <Uniform continuity> of these finitely many iterates turns a sufficiently close <proximal> encounter into a common visit to $U$ after at most $J$ more steps. If the <proximal> encounters occur only at bounded times, a zero distance at some time makes the two future <orbits> coincide, and minimality then gives arbitrarily late common visits. Thus injectivity is not needed for this general lemma.