Lax Lean Archive

Graph families

Lax871432.GraphFamilies · concepts/Lax871432/GraphFamilies.lean · lax-871432

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 finite family of graphs is given by indexing its members: for an index type ι\iota and a bound nn, it assigns to every i∈ιi \in \iota a graph FiF_i on at most nn vertices. Such a family is pairwise non-isomorphic if Fi≇FjF_i \not\cong F_j whenever i≠ji \neq j, and exhaustive if every graph on at most nn vertices is isomorphic to some FiF_i.

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

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Maps
    2
    3/-!
    4---
    5title: Graph families
    6type: definition
    7---
    8A finite family of graphs is given by indexing its members: for an index type ι\iota and a
    9bound nn, it assigns to every i∈ιi \in \iota a graph FiF_i on at most nn vertices. Such a
    10family is *pairwise non-isomorphic* if Fi≇FjF_i \not\cong F_j whenever i≠ji \neq j, and
    11*exhaustive* if every graph on at most nn vertices is isomorphic to some FiF_i.
    12
    13# Implementation notes
    14
    15A *graph family* is an indexed family rather than a set of graphs, so that the index type can
    16be used to address its members. Its graphs have vertex type `Fin (size i)` for sizes bounded
    17by `n`; this is no loss of generality, since every finite family of finite graphs has such a
    18bound, and it keeps matrices over the family indexed by a single type.
    19-/
    20
    21namespace Lax871432.GraphFamilies
    22
    23/-- An *indexed graph family* of order `n`: a family of simple graphs indexed by `ι`, the
    24`i`-th of which has vertex set `Fin (size i)` for some `size i ≤ n`. -/
    25structure GraphFamily (n : ℕ) (ι : Type*) where
    26 /-- The number of vertices of the `i`-th graph. -/
    27 size : ι → ℕ
    28 /-- Every graph in the family has at most `n` vertices. -/
    29 size_le : ∀ i, size i ≤ n
    30 /-- The `i`-th graph of the family. -/
    31 graph : ∀ i, SimpleGraph (Fin (size i))
    32
    33variable {n : ℕ} {ι : Type*}
    34
    35/-- Two indices carry isomorphic graphs. -/
    36def GraphFamily.Iso (F : GraphFamily n ι) (i j : ι) : Prop :=
    37 Nonempty (F.graph i ≃g F.graph j)
    38
    39/-- The graphs in the family are pairwise non-isomorphic. -/
    40def GraphFamily.PairwiseNonIso (F : GraphFamily n ι) : Prop :=
    41 Pairwise fun i j => ¬ F.Iso i j
    42
    43/-- The family represents every isomorphism class of graphs on at most `n` vertices. -/
    44def GraphFamily.IsExhaustive (F : GraphFamily n ι) : Prop :=
    45 ∀ m ≤ n, ∀ G : SimpleGraph (Fin m), ∃ i, Nonempty (G ≃g F.graph i)
    46
    47end Lax871432.GraphFamilies
    48

    Implementation notes

    A graph family is an indexed family rather than a set of graphs, so that the index type can be used to address its members. Its graphs have vertex type Fin(sizei)Fin (size i) for sizes bounded by nn; this is no loss of generality, since every finite family of finite graphs has such a bound, and it keeps matrices over the family indexed by a single type.

    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…