Lax Lean Archive

Digraph representation of simple graphs

Lax683916.DigraphRepresentation · concepts/Lax683916/DigraphRepresentation.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

    Simple graphs on a vertex type VV are equivalent to symmetric loopless digraphs on VV. The equivalence preserves the adjacency relation exactly.

    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 Mathlib.Combinatorics.SimpleGraph.Basic
    2import Lax683916.SymmetricLooplessDigraphs
    3
    4/-!
    5---
    6title: Digraph representation of simple graphs
    7type: theorem
    8---
    9Simple graphs on a vertex type `V` are equivalent to symmetric loopless
    10digraphs on `V`. The equivalence preserves the adjacency relation exactly.
    11
    12# Formalization notes
    13
    14Both structures consist of the same relation and the same two laws. The
    15statement is therefore an equivalence of types, rather than merely a pair of
    16conversions or an isomorphism after changing the vertex type.
    17-/
    18
    19namespace Lax683916.DigraphRepresentation
    20
    21open Lax683916.SymmetricLooplessDigraphs
    22
    23universe u
    24
    25/-- An equivalence that retains exactly the same adjacency relation. -/
    26structure RepresentationEquiv (V : Type u) where
    27 /-- The equivalence between the two representation types. -/
    28 toEquiv : SimpleGraph V ≃ SymmetricLooplessDigraph V
    29 /-- A directed edge in the image is exactly an edge of the original simple graph. -/
    30 map_adj : ∀ (G : SimpleGraph V) (u v : V),
    31 (toEquiv G).graph.Adj u v ↔ G.Adj u v
    32
    33/-- Simple graphs and symmetric loopless digraphs on the same vertices are equivalent. -/
    34axiom simpleGraphEquiv (V : Type u) :
    35 Nonempty (RepresentationEquiv V)
    36
    37end Lax683916.DigraphRepresentation
    38
    Show Proof
    Formalization notes

    Both structures consist of the same relation and the same two laws. The statement is therefore an equivalence of types, rather than merely a pair of conversions or an isomorphism after changing the vertex type.

    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…