Lax Lean Archive

Hypergraph representation of simple graphs

Lax683916.HypergraphRepresentation · concepts/Lax683916/HypergraphRepresentation.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 VV are equivalent to spanning 2-uniform hypergraphs on VV. Graph edges become two-element hyperedges and no vertex is lost.

    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.SpanningTwoUniformHypergraphs
    3
    4/-!
    5---
    6title: Hypergraph representation of simple graphs
    7type: theorem
    8---
    9Simple graphs on `V` are equivalent to spanning 2-uniform hypergraphs on
    10`V`. Graph edges become two-element hyperedges and no vertex is lost.
    11
    12# Formalization notes
    13
    14The representation is an equivalence of types. Spanning fixes the explicit
    15hypergraph vertex set, while 2-uniformity identifies the hyperedge set with
    16the ordinary unordered edges of a simple graph.
    17-/
    18
    19namespace Lax683916.HypergraphRepresentation
    20
    21open Lax683916.SpanningTwoUniformHypergraphs
    22
    23universe u
    24
    25/-- An equivalence that sends graph edges to two-element hyperedges. -/
    26structure RepresentationEquiv (V : Type u) where
    27 /-- The equivalence between the two representation types. -/
    28 toEquiv : SimpleGraph V ≃ SpanningTwoUniformHypergraph V
    29 /-- A pair is a hyperedge in the image exactly when its two elements are adjacent. -/
    30 map_pair : ∀ (G : SimpleGraph V) (u v : V),
    31 {u, v} ∈ (toEquiv G).hypergraph.edgeSet ↔ G.Adj u v
    32
    33/-- Simple graphs and spanning 2-uniform hypergraphs on the same vertices are equivalent. -/
    34axiom simpleGraphEquiv (V : Type u) :
    35 Nonempty (RepresentationEquiv V)
    36
    37end Lax683916.HypergraphRepresentation
    38
    Show Proof
    Formalization notes

    The representation is an equivalence of types. Spanning fixes the explicit hypergraph vertex set, while 2-uniformity identifies the hyperedge set with the ordinary unordered edges of a simple graph.

    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…