Lax Lean Archive

Lax5.GraphClasses

Weakly sparse graph classes

concepts/Lax5/GraphClasses.lean · lax-5

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 claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    A graph class is a set of finite simple graphs: for each number of vertices n, some of the simple graphs on the canonical n-element vertex type. A graph class is weakly sparse if some complete bipartite graph Kt,tK_{t,t} occurs in no member as a subgraph.

    Lean source view on GitHub

    1import Lax12.GraphClasses
    2import Mathlib.Combinatorics.SimpleGraph.Copy
    3
    4/-!
    5---
    6title: Weakly sparse graph classes
    7type: definition
    8---
    9A graph class is a set of finite simple graphs: for each number of
    10vertices *n*, some of the simple graphs on the canonical *n*-element
    11vertex type. A graph class is weakly sparse if some complete bipartite
    12graph Kt,tK_{t,t} occurs in no member as a subgraph.
    13
    14# Formalization notes
    15
    16The notion of a graph class is not restated here. `GraphClass` is the
    17abbreviation of the *Sparsity Lectures* submission (Lax12), imported and
    18used as is, so that the statements of this submission and the statements
    19assumed from that one speak about literally the same objects. This
    20concept adds the two class-level notions this submission needs on top of
    21it: the class of all graphs, which the definition of monadic dependence
    22names as the transduction target, and weak sparseness.
    23
    24Subgraph containment is mathlib's `⊑` (an injective homomorphism of
    25`completeBipartiteGraph (Fin t) (Fin t)` into the member). The value
    26`t = 0` does not trivialize weak sparseness: the empty graph is
    27contained in every graph, so `¬ K_{0,0} ⊑ G` never holds and no side
    28condition on `t` is needed.
    29-/
    30
    31namespace Lax5.GraphClasses
    32
    33open scoped SimpleGraph
    34open Lax12.GraphClasses
    35
    36/-- The class of all finite simple graphs. -/
    37def allGraphs : GraphClass := fun _ _ => True
    38
    39/-- A graph class is weakly sparse if some complete bipartite graph
    40`K_{t,t}` occurs in no member as a subgraph. -/
    41def WeaklySparse (C : GraphClass) : Prop :=
    42 ∃ t : ℕ, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G →
    43 ¬ completeBipartiteGraph (Fin t) (Fin t) ⊑ G
    44
    45end Lax5.GraphClasses
    46

    Formalization notes

    The notion of a graph class is not restated here. GraphClassGraphClass is the abbreviation of the Sparsity Lectures submission (Lax12), imported and used as is, so that the statements of this submission and the statements assumed from that one speak about literally the same objects. This concept adds the two class-level notions this submission needs on top of it: the class of all graphs, which the definition of monadic dependence names as the transduction target, and weak sparseness.

    Subgraph containment is mathlib's ⊑⊑ (an injective homomorphism of completeBipartiteGraph(Fint)(Fint)completeBipartiteGraph (Fin t) (Fin t) into the member). The value t=0t = 0 does not trivialize weak sparseness: the empty graph is contained in every graph, so ¬K0,0⊑G¬ K_{0,0} ⊑ G never holds and no side condition on tt is needed.

    Builds on

    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…