Lax Lean Archive

Simple-graph representation of a simple multigraph

Lax683916.MultigraphRepresentation · concepts/Lax683916/MultigraphRepresentation.lean · lax-683916

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

    Every simple loopless multigraph is a simple graph up to simultaneous isomorphism of its actual vertex and edge sets. Incidence is preserved: an edge has endpoints uu and vv precisely when its image is the unordered edge joining the images of uu and vv.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax683916.MultigraphIsomorphism
    2
    3/-!
    4---
    5title: Simple-graph representation of a simple multigraph
    6type: theorem
    7---
    8Every simple loopless multigraph is a simple graph up to simultaneous
    9isomorphism of its actual vertex and edge sets. Incidence is preserved: an
    10edge has endpoints `u` and `v` precisely when its image is the unordered edge
    11joining the images of `u` and `v`.
    12
    13# Formalization notes
    14
    15The isomorphism notion is supplied by the companion definition concept.
    16Mathlib's `Graph.Simple` already includes looplessness and uniqueness of an
    17edge with given endpoints. The theorem chooses `G.vertexSet` as its canonical
    18simple-graph carrier; the isomorphism definition also permits subsequent
    19changes of vertex type.
    20-/
    21
    22namespace Lax683916.MultigraphRepresentation
    23
    24open Lax683916.MultigraphIsomorphism
    25
    26universe u v
    27
    28/-- Every simple multigraph is isomorphic to a simple graph on its actual vertex set. -/
    29axiom exists_simpleGraph_representation {α : Type u} {β : Type v}
    30 (G : Graph α β) [G.Simple] :
    31 ∃ H : SimpleGraph G.vertexSet, Nonempty (IsomorphicToSimpleGraph G H)
    32
    33end Lax683916.MultigraphRepresentation
    34
    Show Proof
    Formalization notes

    The isomorphism notion is supplied by the companion definition concept. Mathlib's Graph.SimpleGraph.Simple already includes looplessness and uniqueness of an edge with given endpoints. The theorem chooses G.vertexSetG.vertexSet as its canonical simple-graph carrier; the isomorphism definition also permits subsequent changes of vertex type.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…