Proof of `Euler's formula`
groundedproofs/Lax909950Proofs/EulerFormula.lean · lax-909950
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
In the paper
- page 1 of this submission's paper
Description
By induction on the number of edges. A tree has one face. Otherwise some edge lies on a cycle; its two sides lie in different faces, and deleting it merges them.