Lax Lean Archive

Symmetric loopless digraph

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

definition

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

    Definition

    A symmetric loopless digraph is a directed graph in which every arrow is accompanied by its reverse and no vertex has an arrow to itself.

    Concept map
    1 concept; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.Digraph.Basic
    2
    3/-!
    4---
    5title: Symmetric loopless digraph
    6type: definition
    7---
    8A symmetric loopless digraph is a directed graph in which every arrow is
    9accompanied by its reverse and no vertex has an arrow to itself.
    10
    11# Formalization notes
    12
    13The directed graph is bundled with symmetry and irreflexivity of its
    14adjacency relation. These are exactly the two laws carried by a simple graph,
    15but the bundle keeps the underlying object visibly in `Digraph V`.
    16-/
    17
    18namespace Lax683916.SymmetricLooplessDigraphs
    19
    20/-- A directed graph whose adjacency relation is symmetric and irreflexive. -/
    21structure SymmetricLooplessDigraph (V : Type*) where
    22 /-- The underlying directed graph. -/
    23 graph : Digraph V
    24 /-- Every directed edge occurs in both orientations. -/
    25 symm : Std.Symm graph.Adj
    26 /-- No vertex is adjacent to itself. -/
    27 loopless : Std.Irrefl graph.Adj
    28
    29end Lax683916.SymmetricLooplessDigraphs
    30
    Formalization notes

    The directed graph is bundled with symmetry and irreflexivity of its adjacency relation. These are exactly the two laws carried by a simple graph, but the bundle keeps the underlying object visibly in DigraphVDigraph V.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…