Lax Lean Archive

Balls around vertex sets in a graph

Lax185574.GraphBalls · concepts/Lax185574/GraphBalls.lean · lax-185574

definition

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

    Definition

    For a graph G, a radius r ∈ ℕ and a set C ⊆ V(G), the ball

    Ball^G_r[C] = { w ∈ V(G) : dist^G(c, w) ≤ r for some c ∈ C }

    is the union of the balls Ball^G_r[c] of radius r around the vertices c ∈ C. For a vertex v it is written Ball^G_r[v], and for a tuple v̄ it is the ball around the set of entries of v̄.

    The distance between two sets is the minimum distance between their elements. So dist^G(X, A) > r holds if and only if Ball^G_r[X] is disjoint from A.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    In the paper

    • page 12 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.GaifmanGraph
    2
    3/-!
    4---
    5title: Balls around vertex sets in a graph
    6type: definition
    7---
    8For a graph G, a radius r ∈ ℕ and a set C ⊆ V(G), the ball
    9
    10Ball^G_r[C] = { w ∈ V(G) : dist^G(c, w) ≤ r for some c ∈ C }
    11
    12is the union of the balls Ball^G_r[c] of radius r around the vertices
    13c ∈ C. For a vertex v it is written Ball^G_r[v], and for a tuple v̄ it
    14is the ball around the set of entries of v̄.
    15
    16The distance between two sets is the minimum distance between their
    17elements. So dist^G(X, A) > r holds if and only if Ball^G_r[X] is
    18disjoint from A.
    19
    20# Formalization notes
    21
    22The ball is defined for a simple graph and an arbitrary set of centers.
    23"Distance at most r" is `GaifmanGraph.WithinDist`, a walk of length at
    24most r. Vertices in different components are at infinite distance. The
    25paper writes the closed ball defined here as Ball^G_r(v).
    26
    27Statements of the form dist^G(X, A) > r, for sets or for the entries of
    28a tuple, are expressed as disjointness of Ball^G_r[X] and A. This
    29matches the paper's own reformulation of separation as an empty
    30intersection of a ball with a set. If A is empty, the distance is
    31infinite and the condition holds.
    32-/
    33
    34namespace Lax185574.GraphBalls
    35
    36open Lax185574.GaifmanGraph
    37
    38universe u
    39
    40variable {V : Type u}
    41
    42/-- `Ball^G_r[C]`: the vertices within distance `r` of some vertex of
    43`C`. -/
    44def graphBall (G : SimpleGraph V) (r : ℕ) (C : Set V) : Set V :=
    45 {w | ∃ c ∈ C, WithinDist G r c w}
    46
    47end Lax185574.GraphBalls
    48
    Formalization notes

    The ball is defined for a simple graph and an arbitrary set of centers. "Distance at most r" is GaifmanGraph.WithinDistGaifmanGraph.WithinDist, a walk of length at most r. Vertices in different components are at infinite distance. The paper writes the closed ball defined here as Ball^G_r(v).

    Statements of the form dist^G(X, A) > r, for sets or for the entries of a tuple, are expressed as disjointness of Ball^G_r[X] and A. This matches the paper's own reformulation of separation as an empty intersection of a ball with a set. If A is empty, the distance is infinite and the condition holds.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…