Lax Lean Archive

Lax12.GraphClasses

Graph classes

concepts/Lax12/GraphClasses.lean · lax-12

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.

    Concept map

    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    A graph class is a set of finite simple graphs. A class contains, for each number of vertices n, some of the simple graphs on the canonical n-element vertex type.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2
    3/-!
    4---
    5title: Graph classes
    6type: definition
    7---
    8A graph class is a set of finite simple graphs. A class contains, for
    9each number of vertices *n*, some of the simple graphs on the canonical
    10*n*-element vertex type.
    11
    12# Formalization notes
    13
    14Every finite simple graph is isomorphic to a graph on some `Fin n`, so
    15ranging over the canonical carriers loses no generality. Closure under
    16isomorphism is deliberately not required: no statement of this
    17submission needs it, and all hypotheses range over concrete members.
    18`GraphClass` is an abbreviation, so class membership is plain
    19application `C n G` throughout the submission, and any identically
    20shaped abbreviation elsewhere denotes literally the same function type.
    21-/
    22
    23namespace Lax12.GraphClasses
    24
    25/-- A class of finite simple graphs: for each number of vertices `n`, a
    26predicate on the simple graphs over the canonical `n`-element type. -/
    27abbrev GraphClass : Type := ∀ n : ℕ, SimpleGraph (Fin n) → Prop
    28
    29end Lax12.GraphClasses
    30

    Formalization notes

    Every finite simple graph is isomorphic to a graph on some FinnFin n, so ranging over the canonical carriers loses no generality. Closure under isomorphism is deliberately not required: no statement of this submission needs it, and all hypotheses range over concrete members. GraphClassGraphClass is an abbreviation, so class membership is plain application CnGC n G throughout the submission, and any identically shaped abbreviation elsewhere denotes literally the same function type.

    Builds on

    none

    Used by

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…