Sum of plane face degrees
ProvedSumFaceDegreesThe sum of the degrees of all indexed faces in crossing-free plane face data equals twice the number of graph edges, since each edge contributes two darts.
Preamble
import Definitions.Def_PlaneFaceData open Classical noncomputable section
Formal statement
lemma SumFaceDegrees {V : Type*} [Fintype V] (G : SimpleGraph V)
[Fintype G.edgeSet] [DecidableRel G.Adj] (D : OrdinaryPolygonalDrawing G)
(hD : D.crossingSet.card = 0) (A : PlaneFaceData G D) :
((@Finset.univ A.Face A.faceFintype).sum A.faceDegree) =
2 * G.edgeFinset.card := by sorrySource