Lax Lean Archive

Balls of the pair relation lie in flip-metric balls

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

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

    Lemma

    Fix a graph G and a partition 𝒫 of V(G), and let R ≔ R(G, 𝒫). For every radius r ∈ ℕ and vertex v ∈ V(G),

    Ball^R_r(v) ⊆ Ball^𝒫_{5r}(v).

    Concept map
    12 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 34 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.PairRelation
    2import Lax185574.Flips
    3import Lax185574.GraphBalls
    4
    5/-!
    6---
    7title: Balls of the pair relation lie in flip-metric balls
    8type: lemma
    9---
    10Fix a graph G and a partition 𝒫 of V(G), and let R ≔ R(G, 𝒫). For every
    11radius r ∈ ℕ and vertex v ∈ V(G),
    12
    13Ball^R_r(v) ⊆ Ball^𝒫_{5r}(v).
    14
    15# Formalization notes
    16
    17Ball^R_r(v) is the ball in the graph R, `GraphBalls.graphBall`, around
    18the single vertex v. Ball^𝒫_{5r}(v) is the ball of the 𝒫-flip metric,
    19`Flips.flipBall`.
    20-/
    21
    22namespace Lax185574.PairRelationBalls
    23
    24open Lax185574.PairRelation Lax185574.Flips Lax185574.GraphBalls
    25
    26universe z
    27
    28/-- **Ball containment.** A radius-`r` ball of `R(G, 𝒫)` lies in the
    29radius-`5r` ball of the `𝒫`-flip metric. -/
    30axiom graphBall_pairRelation_subset {V : Type z} (G : SimpleGraph V) (P : Setoid V)
    31 (r : ℕ) (v : V) :
    32 graphBall (pairRelation G P) r {v} ⊆ flipBall G P (5 * r) v
    33
    34end Lax185574.PairRelationBalls
    35
    Show Proof
    Formalization notes

    Ball^R_r(v) is the ball in the graph R, GraphBalls.graphBallGraphBalls.graphBall, around the single vertex v. Ball^𝒫_{5r}(v) is the ball of the 𝒫-flip metric, Flips.flipBallFlips.flipBall.

    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…