Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Hereditary graph classes

Lax263307.GraphClasses · concepts/Lax263307/GraphClasses.lean · lax-263307

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 class of finite simple graphs is hereditary if it is closed under taking induced subgraphs and under isomorphism.

    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.Maps
    2
    3/-!
    4---
    5title: Hereditary graph classes
    6type: definition
    7---
    8A class of finite simple graphs is hereditary if it is closed under taking
    9induced subgraphs and under isomorphism.
    10
    11# Formalization notes
    12
    13Graphs are represented on vertex sets {0,…,n−1}\{0,\ldots,n-1\}. Closure under
    14induced embeddings includes both induced subgraphs and all relabelings.
    15No algorithm for recognizing membership in the class is assumed.
    16-/
    17
    18namespace Lax263307.GraphClasses
    19
    20/-- A class of finite simple graphs, represented on numbered vertex sets. -/
    21abbrev GraphClass := (n : ℕ) → Set (SimpleGraph (Fin n))
    22
    23/-- Every graph that embeds as an induced subgraph of a member also belongs. -/
    24def IsHereditary (C : GraphClass) : Prop :=
    25 ∀ (m n : ℕ) (H : SimpleGraph (Fin m)) (G : SimpleGraph (Fin n)),
    26 G ∈ C n → Nonempty (H ↪g G) → H ∈ C m
    27
    28end Lax263307.GraphClasses
    29
    Formalization notes

    Graphs are represented on vertex sets {0,…,n−1}\{0,\ldots,n-1\}. Closure under induced embeddings includes both induced subgraphs and all relabelings. No algorithm for recognizing membership in the class is assumed.

    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…