Lax Lean Archive

Graphs and graph classes

Lax185574.Graphs · concepts/Lax185574/Graphs.lean · lax-185574

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 graph has the vertices 0, 1, …, n − 1 for some n and a symmetric and irreflexive adjacency relation. A graph class is a set of graphs.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2
    3/-!
    4---
    5title: Graphs and graph classes
    6type: definition
    7---
    8A *graph* has the vertices 0, 1, …, n − 1 for some n and a symmetric
    9and irreflexive adjacency relation. A *graph class* is a set of graphs.
    10
    11# Formalization notes
    12
    13The vertex count is part of the graph, so that a graph class is simply
    14a set of graphs and a graph can be passed to an algorithm as one value.
    15The fields are those of mathlib's `SimpleGraph` on `Fin n`, written out
    16so that the definition can be read without knowing mathlib.
    17
    18The notions of graph theory in this submission are stated for mathlib's
    19`SimpleGraph`, whose library they use. A graph is turned into one by
    20`Graph.toSimpleGraph`, which keeps the vertices and the adjacency.
    21Conversely, `Graph.ofSimpleGraph` turns a simple graph on the vertices
    220, 1, …, n − 1 into a graph.
    23
    24A graph class need not be closed under isomorphism. Every notion applied
    25to graph classes in this submission is invariant under isomorphism
    26anyway.
    27-/
    28
    29namespace Lax185574.Graphs
    30
    31/-- A graph on the vertices `0, 1, …, n - 1`. -/
    32structure Graph where
    33 /-- The number of vertices. -/
    34 n : ℕ
    35 /-- The adjacency relation. -/
    36 Adj : Fin n → Fin n → Prop
    37 /-- Adjacency is symmetric. -/
    38 symm : ∀ u v, Adj u v → Adj v u
    39 /-- No vertex is adjacent to itself. -/
    40 loopless : ∀ v, ¬ Adj v v
    41
    42/-- A graph class: a set of graphs. -/
    43abbrev GraphClass : Type := Set Graph
    44
    45/-- The graph `G` as a mathlib `SimpleGraph` on its vertices
    46`0, 1, …, n - 1`, with the same adjacency. -/
    47def Graph.toSimpleGraph (G : Graph) : SimpleGraph (Fin G.n) where
    48 Adj := G.Adj
    49 symm := ⟨G.symm⟩
    50 loopless := ⟨G.loopless⟩
    51
    52/-- The mathlib `SimpleGraph` `H` on the vertices `0, 1, …, n - 1` as a
    53graph, with the same adjacency. -/
    54def Graph.ofSimpleGraph {n : ℕ} (H : SimpleGraph (Fin n)) : Graph :=
    55 ⟨n, H.Adj, fun _ _ h => H.adj_symm h, fun _ => H.irrefl⟩
    56
    57end Lax185574.Graphs
    58
    Formalization notes

    The vertex count is part of the graph, so that a graph class is simply a set of graphs and a graph can be passed to an algorithm as one value. The fields are those of mathlib's SimpleGraphSimpleGraph on FinnFin n, written out so that the definition can be read without knowing mathlib.

    The notions of graph theory in this submission are stated for mathlib's SimpleGraphSimpleGraph, whose library they use. A graph is turned into one by Graph.toSimpleGraphGraph.toSimpleGraph, which keeps the vertices and the adjacency. Conversely, Graph.ofSimpleGraphGraph.ofSimpleGraph turns a simple graph on the vertices 0, 1, …, n − 1 into a graph.

    A graph class need not be closed under isomorphism. Every notion applied to graph classes in this submission is invariant under isomorphism anyway.

    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…