Right continuity of percolation probability (source code)

= Right continuity of percolation probability

For independent <site percolation> or <bond percolation> on a rooted <locally finite graph>, $\theta(p)$ is right continuous on $[0,1)$. Finite-radius connection events have polynomial <probabilities> in $p$ and decrease to infinite connection. Thus $\theta$ is their infimum by <continuity from above of a measure>. This infimum of <continuous functions> is upper semicontinuous; parameter monotonicity from the <monotone coupling of Bernoulli percolation> then gives right continuity.