Graph exhaustion (source code)

= Graph exhaustion
{title2=$V_1\subseteq V_2\subseteq\cdots,\quad\bigcup_nV_n=V$}

An exhaustion of a countable <graph> is an increasing <sequence> of finite connected <graph vertex> sets whose union is the whole <graph vertex> set. In a <locally finite graph>, every prescribed finite <graph path> together with all <graph neighbours> of its visited <graph vertices> lies in a sufficiently large exhaustion set. This permits coupling finite-volume and infinite-volume <simple random walks> up to a finite stopping time.