Lax Lean Archive

Weakly sparse monadically dependent classes are nowhere dense

Lax710763.WeaklySparseDependent · concepts/Lax710763/WeaklySparseDependent.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 weakly sparse monadically dependent graph class is nowhere dense. Together with the statement that nowhere dense classes are monadically dependent, 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.GraphClasses
    2import Lax710763.MonadicDependence
    3import Lax199508.NowhereDenseClasses
    4
    5/-!
    6---
    7title: Weakly sparse monadically dependent classes are nowhere dense
    8type: theorem
    9---
    10Every weakly sparse monadically dependent graph class is nowhere dense.
    11Together with the statement that nowhere dense classes are monadically
    12dependent, this carries the classical equivalence: on weakly sparse
    13classes, monadic dependence and nowhere denseness coincide.
    14
    15# Formalization notes
    16
    17The hypotheses are the weak sparseness predicate of the graph classes
    18concept of this submission and the transduction-based definition of
    19monadic dependence; the conclusion is `NowhereDense`, the shallow-minor
    20definition of the *Sparsity Lectures* submission (Lax199508), where nowhere
    21denseness is defined and endorsed. Stating the conclusion over that
    22definition is what lets this statement compose directly with the
    23sparsity theory built on it.
    24-/
    25
    26namespace Lax710763.WeaklySparseDependent
    27
    28open Lax199508.GraphClasses Lax199508.NowhereDenseClasses
    29open Lax710763.GraphClasses Lax710763.MonadicDependence
    30
    31/-- Every weakly sparse monadically dependent graph class is nowhere
    32dense. -/
    33axiom nowhereDense_of_weaklySparse_of_monadicallyDependent
    34 (C : GraphClass) (hs : WeaklySparse C) (hd : MonadicallyDependent C) :
    35 NowhereDense C
    36
    37end Lax710763.WeaklySparseDependent
    38
    Show Proof
    Formalization notes

    The hypotheses are the weak sparseness predicate of the graph classes concept of this submission and the transduction-based definition of monadic dependence; the conclusion is NowhereDenseNowhereDense, the shallow-minor definition of the Sparsity Lectures submission (Lax199508), where nowhere denseness is defined and endorsed. Stating the conclusion over that definition is what lets this statement compose directly with the sparsity theory built on it.

    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…