Lax Lean Archive

Lax12.NowhereDenseUQW

Nowhere dense classes are uniformly quasi-wide

concepts/Lax12/NowhereDenseUQW.lean · lax-12

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 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.

    Lean source view on GitHub

    1import Lax12.NowhereDenseClasses
    2import Lax12.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 Lax12.NowhereDenseUQW
    31
    32open Lax12.GraphClasses Lax12.NowhereDenseClasses Lax12.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 Lax12.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

    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…