Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Characterization of Label-Connected Multigraphs

Lax630294.Characterization · concepts/Lax630294/Characterization.lean · lax-630294

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

    Let GG be a finite multigraph. Then GG is a yes-instance of Gossiping (label-connected) if and only if at least one of the following holds:

    1. GG has at most one vertex;
    2. GG is a TT-graph;
    3. GG is an MM-graph.
    Concept map
    5 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 5 of this submission's paper

    Lean source view on GitHub

    1import Lax630294.Gossiping
    2import Lax630294.TGraph
    3import Lax630294.MGraph
    4
    5/-!
    6---
    7title: Characterization of Label-Connected Multigraphs
    8type: theorem
    9---
    10
    11Let `G` be a finite multigraph. Then `G` is a yes-instance of Gossiping
    12(label-connected) if and only if at least one of the following holds:
    13
    141. `G` has at most one vertex;
    152. `G` is a `T`-graph;
    163. `G` is an `M`-graph.
    17
    18# Formalization notes
    19
    20Multigraphs are Mathlib's `Graph α β`; finiteness of the vertex set and of the
    21edge set is assumed. The definitions of label-connectedness, `T`-graphs and
    22`M`-graphs are those of the concepts `Gossiping`, `TGraph` and `MGraph`. Loops are
    23allowed in `G`; they play no role on either side of the equivalence.
    24-/
    25
    26namespace Lax630294.Characterization
    27
    28open Graph Lax630294.Gossiping Lax630294.TGraph Lax630294.MGraph
    29
    30universe u v
    31
    32/-- A finite multigraph is label-connected if and only if it has at most one vertex,
    33is a `T`-graph, or is an `M`-graph. -/
    34axiom isLabelConnected_iff {α : Type u} {β : Type v} (G : Graph α β)
    35 (hV : V(G).Finite) (hE : E(G).Finite) :
    36 IsLabelConnected G ↔ V(G).Subsingleton ∨ IsTGraph G ∨ IsMGraph G
    37
    38end Lax630294.Characterization
    39
    Show Proof
    Formalization notes

    Multigraphs are Mathlib's GraphαβGraph α β; finiteness of the vertex set and of the edge set is assumed. The definitions of label-connectedness, TT-graphs and MM-graphs are those of the concepts GossipingGossiping, TGraphTGraph and MGraphMGraph. Loops are allowed in GG; they play no role on either side of the equivalence.

    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…