Planar graph edge bound (source code)

= Planar graph edge bound
{title2=$m\leq3n-6$}

A finite <simple graph> that is a <connected graph> and a <planar graph>, with $n\geq3$ <vertices> and $m$ <edges>, satisfies $m\leq3n-6$. Choose a <plane graph>: each <facial boundary walk> has length at least three, so $3f\leq2m$. Substitute $f=2-n+m$ from the <Euler formula for a connected planar graph>.<Mathematics for Computer Science by Eric Lehman and others>[Mathematics for Computer Science, §12.4, Lemma 12.4.2 and Theorem 12.4.3, printed pp. 485–486]{ref}

The <complete graph> $K_4$ attains equality: $6=3\cdot4-6$. The bound also holds for a disconnected finite <simple graph> that is a <planar graph> with $n\geq3$: place its <connected components of a graph> in disjoint regions and join them with new <bridges in a graph>, then apply the connected bound.