Lax Lean Archive

Lax5.AdlerAdler

Nowhere dense classes are monadically dependent

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    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.

    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

    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…