Formal definition of "planar graph"

There are a number of ways. For example, we could have an injective function $f : V(G) \to \mathbb R^2$ giving the coordinates of the vertices. For every edge $vw \in E(G)$, we could have a path from $f(v)$ to $f(w)$: a continuous function $h_{vw} : [0,1] \to \mathbb R^2$ with $h_{vw}(0) = f(v)$ and $h_{vw}(1) = f(w)$. To ensure that the edges don't cross, we could require that for two edges $e_1, e_2$ the corresponding functions $h_1$, $h_2$ don't have $h_1(s) = h_2(t)$ unless both $s$ and $t$ are either $0$ or $1$.

Because the specific topological definition doesn't affect the combinatorial meaning too much, we can play around with this definition to get something easier to work with. For example, rather than making $h_{vw}$ continuous, we could ask for it to be smooth, or piecewise linear. The goal would be to make it easier to prove obvious-sounding geometrical properties of the embedding. For example, you might not want to invoke the Jordan curve theorem just to say that every cycle in the graph has an inside and an outside.

Ultimately, we leave these details out of the definition because the details don't matter much - various ways to fill in the details produce the same notion of planar graphs.

In fact, since every planar graph has a straight-line embedding, we could even make the edges be line segments $[f(v), f(w)]$ and require their interiors to be disjoint. But this is probably less convenient to work with.