Lax Lean Archive

Nowhere dense classes are uniformly quasi-wide

Lax199508.NowhereDenseUQW · concepts/Lax199508/NowhereDenseUQW.lean · lax-199508

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 uniformly quasi-wide: for every radius r there are a threshold function N and a separator bound s such that in every member, every vertex set of size at least N(m) contains a distance-r independent subset of size at least m after deleting at most s vertices.

    This is Lemma 3.4 of Chapter 4 of the source lecture notes (2019/20 edition), the hard direction of their Theorem 3.2, which states that a graph class is uniformly quasi-wide if and only if it is nowhere dense.

    Concept map
    4 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 Lax199508.NowhereDenseClasses
    2import Lax199508.UniformQuasiWideness
    3
    4/-!
    5---
    6title: Nowhere dense classes are uniformly quasi-wide
    7type: theorem
    8---
    9Every nowhere dense graph class is uniformly quasi-wide: for every
    10radius *r* there are a threshold function *N* and a separator bound *s*
    11such that in every member, every vertex set of size at least *N*(*m*)
    12contains a distance-*r* independent subset of size at least *m* after
    13deleting at most *s* vertices.
    14
    15This is Lemma 3.4 of Chapter 4 of the source lecture notes (2019/20
    16edition), the hard direction of their Theorem 3.2, which states that a
    17graph class is uniformly quasi-wide if and only if it is nowhere dense.
    18
    19# Formalization notes
    20
    21Hypothesis and conclusion are the shared predicates of the two imported
    22definition concepts, so the statement adds nothing of its own. The
    23strength of the theorem is entirely in the quantifier order already
    24carried by `UniformlyQuasiWide`: the separator bound depends on the
    25class and the radius alone, not on the requested size or on the member.
    26The converse implication holds on subgraph-closed classes but is a
    27separate claim with a separate proof and is not stated here.
    28-/
    29
    30namespace Lax199508.NowhereDenseUQW
    31
    32open Lax199508.GraphClasses Lax199508.NowhereDenseClasses Lax199508.UniformQuasiWideness
    33
    34/-- Nowhere dense graph classes are uniformly quasi-wide. -/
    35axiom uniformlyQuasiWide_of_nowhereDense
    36 (C : GraphClass) (h : NowhereDense C) :
    37 UniformlyQuasiWide C
    38
    39end Lax199508.NowhereDenseUQW
    40
    Show Proof
    Formalization notes

    Hypothesis and conclusion are the shared predicates of the two imported definition concepts, so the statement adds nothing of its own. The strength of the theorem is entirely in the quantifier order already carried by UniformlyQuasiWideUniformlyQuasiWide: the separator bound depends on the class and the radius alone, not on the requested size or on the member. The converse implication holds on subgraph-closed classes but is a separate claim with a separate proof and is not stated here.

    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…