Lax Lean Archive

Neighborhood-set-system representation of simple graphs

Lax683916.NeighborhoodSetSystemRepresentation · concepts/Lax683916/NeighborhoodSetSystemRepresentation.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 symmetric loopless neighborhood set systems indexed by VV. The set assigned to uu is exactly its open neighborhood.

    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.NeighborhoodSetSystems
    3
    4/-!
    5---
    6title: Neighborhood-set-system representation of simple graphs
    7type: theorem
    8---
    9Simple graphs on `V` are equivalent to symmetric loopless neighborhood set
    10systems indexed by `V`. The set assigned to `u` is exactly its open
    11neighborhood.
    12
    13# Formalization notes
    14
    15The equivalence retains the vertex type and adjacency relation exactly. An
    16unindexed family `Set (Set V)` would forget which vertex owns a neighborhood,
    17so the vertex indexing is essential for an equivalence with all simple
    18graphs.
    19-/
    20
    21namespace Lax683916.NeighborhoodSetSystemRepresentation
    22
    23open Lax683916.NeighborhoodSetSystems
    24
    25universe u
    26
    27/-- An equivalence that sends every graph to its vertex-indexed open neighborhoods. -/
    28structure RepresentationEquiv (V : Type u) where
    29 /-- The equivalence between simple graphs and neighborhood set systems. -/
    30 toEquiv : SimpleGraph V ≃ NeighborhoodSetSystem V
    31 /-- Membership in the image neighborhood is exactly adjacency. -/
    32 map_mem : ∀ (G : SimpleGraph V) (u v : V),
    33 v ∈ (toEquiv G).neighborhood u ↔ G.Adj u v
    34
    35/-- Simple graphs and symmetric loopless neighborhood set systems are equivalent. -/
    36axiom simpleGraphEquiv (V : Type u) :
    37 Nonempty (RepresentationEquiv V)
    38
    39end Lax683916.NeighborhoodSetSystemRepresentation
    40
    Show Proof
    Formalization notes

    The equivalence retains the vertex type and adjacency relation exactly. An unindexed family Set(SetV)Set (Set V) would forget which vertex owns a neighborhood, so the vertex indexing is essential for an equivalence with all simple graphs.

    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…