Lax Lean Archive

Version history

Submission versions

  1. lax-710763current version

    Almost Linear Neighborhood Complexity of Monadically Dependent Graph Classes

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceOpen version
  2. lax-5viewing

    Almost Linear Neighborhood Complexity of Monadically Dependent Graph Classes

    Created Lean v4.30.0mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f
    GitHub sourceShown on this page

Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.

Nowhere dense classes are monadically dependent

Lax5.AdlerAdler · concepts/Lax5/AdlerAdler.lean · lax-5

proven

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

    Theorem

    Every nowhere dense graph class is monadically dependent. Together with the statement that weakly sparse monadically dependent classes are nowhere dense, this carries the classical equivalence: on weakly sparse classes, monadic dependence and nowhere denseness coincide.

    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax5.MonadicDependence
    2import Lax12.NowhereDenseClasses
    3
    4/-!
    5---
    6title: Nowhere dense classes are monadically dependent
    7type: theorem
    8---
    9Every nowhere dense graph class is monadically dependent. Together with
    10the statement that weakly sparse monadically dependent classes are
    11nowhere dense, this carries the classical equivalence: on weakly sparse
    12classes, monadic dependence and nowhere denseness coincide.
    13
    14# Formalization notes
    15
    16Adler and Adler proved that nowhere dense classes are monadically
    17*stable*; monadic dependence is the weakening stated here, which is how
    18the equivalence is used in the literature. The hypothesis is
    19`NowhereDense`, the shallow-minor definition of the *Sparsity Lectures*
    20submission (Lax12), where nowhere denseness is defined and endorsed.
    21-/
    22
    23namespace Lax5.AdlerAdler
    24
    25open Lax12.GraphClasses Lax12.NowhereDenseClasses
    26open Lax5.MonadicDependence
    27
    28/-- Nowhere dense graph classes are monadically dependent. -/
    29axiom monadicallyDependent_of_nowhereDense
    30 (C : GraphClass) (h : NowhereDense C) :
    31 MonadicallyDependent C
    32
    33end Lax5.AdlerAdler
    34
    Show Proof
    Formalization notes

    Adler and Adler proved that nowhere dense classes are monadically stable; monadic dependence is the weakening stated here, which is how the equivalence is used in the literature. The hypothesis is NowhereDenseNowhereDense, the shallow-minor definition of the Sparsity Lectures submission (Lax12), where nowhere denseness is defined and endorsed.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…