Lax Lean Archive

A graph or its complement has diameter at most 3

Lax185574.ComplementDiameter · concepts/Lax185574/ComplementDiameter.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

    For every graph G, at least one of G and Ḡ has diameter at most 3.

    This is folklore.

    Concept map
    2 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 32 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.GaifmanGraph
    2
    3/-!
    4---
    5title: A graph or its complement has diameter at most 3
    6type: lemma
    7---
    8For every graph G, at least one of G and Ḡ has diameter at most 3.
    9
    10This is folklore.
    11
    12# Formalization notes
    13
    14"Diameter at most 3" says that any two vertices are joined by a walk of
    15length at most 3, `WithinDist` of `Lax185574.GaifmanGraph`. The
    16complement Ḡ is the complement `Gᶜ`, whose edges are the pairs of
    17distinct non-adjacent vertices. The graph may be infinite.
    18-/
    19
    20namespace Lax185574.ComplementDiameter
    21
    22open Lax185574.GaifmanGraph
    23
    24universe z
    25
    26/-- **A graph or its complement has diameter at most 3.** -/
    27axiom diameter_le_three_or_compl {V : Type z} (G : SimpleGraph V) :
    28 (∀ u v : V, WithinDist G 3 u v) ∨ (∀ u v : V, WithinDist Gᶜ 3 u v)
    29
    30end Lax185574.ComplementDiameter
    31
    Show Proof
    Formalization notes

    "Diameter at most 3" says that any two vertices are joined by a walk of length at most 3, WithinDistWithinDist of Lax185574.GaifmanGraphLax185574.GaifmanGraph. The complement Ḡ is the complement GcGᶜ, whose edges are the pairs of distinct non-adjacent vertices. The graph may be infinite.

    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…