Lax Lean Archive

Lax5.WeaklySparseDependent

Weakly sparse monadically dependent classes are nowhere dense

concepts/Lax5/WeaklySparseDependent.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 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.

    Lean source view on GitHub

    1import Lax5.GraphClasses
    2import Lax5.MonadicDependence
    3import Lax12.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 (Lax12), 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 Lax5.WeaklySparseDependent
    27
    28open Lax12.GraphClasses Lax12.NowhereDenseClasses
    29open Lax5.GraphClasses Lax5.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 Lax5.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 (Lax12), 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

    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…