Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Euler's formula

Lax909950.EulerFormula · concepts/Lax909950/EulerFormula.lean · lax-909950

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let GG be a finite connected graph with a crossing-free straight-line drawing in the plane. The faces of the drawing are the connected components of the plane after removing all drawn points and edge segments. If the drawing has vv vertices, ee edges and ff faces, then

    v−e+f=2.v - e + f = 2.

    The formula is stated as v+f=e+2v + f = e + 2 in the extended natural numbers, so that it also asserts that the number of faces is finite.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 1 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Data.Set.Card
    2import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
    3import Mathlib.Topology.Connected.Basic
    4import Mathlib.Topology.Instances.Real.Lemmas
    5import Lax68.StraightLineDrawings
    6
    7/-!
    8---
    9title: Euler's formula
    10type: theorem
    11---
    12Let GG be a finite connected graph with a crossing-free straight-line drawing
    13in the plane. The *faces* of the drawing are the connected components of the
    14plane after removing all drawn points and edge segments. If the drawing has
    15vv vertices, ee edges and ff faces, then
    16v−e+f=2.v - e + f = 2.
    17
    18The formula is stated as v+f=e+2v + f = e + 2 in the extended natural numbers, so
    19that it also asserts that the number of faces is finite.
    20-/
    21
    22set_option autoImplicit false
    23
    24namespace Lax909950.EulerFormula
    25
    26open Lax68.StraightLineDrawings
    27
    28/-- The points of the plane covered by a straight-line drawing: the points of
    29the vertices together with the segments of the edges. -/
    30def image {V : Type*} {G : SimpleGraph V} (D : StraightLineDrawing G) : Set Point :=
    31 Set.range D.point ∪ ⋃ (a : V) (b : V) (_ : G.Adj a b), segment ℝ (D.point a) (D.point b)
    32
    33/-- The faces of a straight-line drawing: the connected components of the
    34complement of its image. -/
    35def faces {V : Type*} {G : SimpleGraph V} (D : StraightLineDrawing G) : Set (Set Point) :=
    36 {F | ∃ x ∉ image D, F = connectedComponentIn (image D)ᶜ x}
    37
    38/-- Euler's formula: a crossing-free straight-line drawing of a finite connected
    39graph with vv vertices and ee edges has exactly ff faces, where
    40v+f=e+2v + f = e + 2. -/
    41axiom euler_formula {V : Type*} [Finite V] {G : SimpleGraph V}
    42 (hG : G.Connected) (D : StraightLineDrawing G) :
    43 (Nat.card V : ℕ∞) + (faces D).encard = G.edgeSet.encard + 2
    44
    45end Lax909950.EulerFormula
    46
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…