Lax Lean Archive

Set-system representation of simple graphs

Lax683916.SetSystemRepresentation · concepts/Lax683916/SetSystemRepresentation.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 2-uniform set systems on VV: an edge with endpoints uu and vv is represented by the two-element set u,v{u, v}.

    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.TwoUniformSetSystems
    3
    4/-!
    5---
    6title: Set-system representation of simple graphs
    7type: theorem
    8---
    9Simple graphs on `V` are equivalent to 2-uniform set systems on `V`: an edge
    10with endpoints `u` and `v` is represented by the two-element set `{u, v}`.
    11
    12# Formalization notes
    13
    14The equivalence uses ordinary sets rather than `Sym2 V`, matching the usual
    15set-system language. The 2-uniformity proof ensures that every member has a
    16unique interpretation as an unordered pair of distinct vertices.
    17-/
    18
    19namespace Lax683916.SetSystemRepresentation
    20
    21open Lax683916.TwoUniformSetSystems
    22
    23universe u
    24
    25/-- An equivalence that sends graph edges to their two-element endpoint sets. -/
    26structure RepresentationEquiv (V : Type u) where
    27 /-- The equivalence between the two representation types. -/
    28 toEquiv : SimpleGraph V ≃ TwoUniformSetSystem V
    29 /-- A pair belongs to the image set system exactly when its two elements are adjacent. -/
    30 map_pair : ∀ (G : SimpleGraph V) (u v : V),
    31 {u, v} ∈ (toEquiv G).sets ↔ G.Adj u v
    32
    33/-- Simple graphs and 2-uniform set systems on the same ground type are equivalent. -/
    34axiom simpleGraphEquiv (V : Type u) :
    35 Nonempty (RepresentationEquiv V)
    36
    37end Lax683916.SetSystemRepresentation
    38
    Show Proof
    Formalization notes

    The equivalence uses ordinary sets rather than Sym2VSym2 V, matching the usual set-system language. The 2-uniformity proof ensures that every member has a unique interpretation as an unordered pair of distinct vertices.

    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…