Lax Lean Archive

Nowhere dense classes are monadically dependent

Lax710763.AdlerAdler · concepts/Lax710763/AdlerAdler.lean · lax-710763

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 Lax710763.MonadicDependence
    2import Lax199508.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 (Lax199508), where nowhere denseness is defined and endorsed.
    21-/
    22
    23namespace Lax710763.AdlerAdler
    24
    25open Lax199508.GraphClasses Lax199508.NowhereDenseClasses
    26open Lax710763.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 Lax710763.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 (Lax199508), 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…