Lax Lean Archive

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

T-Graph

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

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

    A TT-witness of a multigraph GG is a pair of spanning trees of GG that share at most one edge. A multigraph is a TT-graph if it has a TT-witness.

    Concept map
    2 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax630294.SpanningStructures
    2
    3/-!
    4---
    5title: T-Graph
    6type: definition
    7---
    8
    9A *`T`-witness* of a multigraph `G` is a pair of spanning trees of `G` that share
    10at most one edge. A multigraph is a *`T`-graph* if it has a `T`-witness.
    11
    12# Formalization notes
    13
    14The two trees are given by their edge sets `T₁` and `T₂`; they may coincide only
    15when they have at most one edge in common, that is, when `G` has at most two
    16vertices.
    17-/
    18
    19namespace Lax630294.TGraph
    20
    21open Graph Lax630294.SpanningStructures
    22
    23variable {α β : Type*}
    24
    25/-- `T₁, T₂` are spanning trees of `G` sharing at most one edge. -/
    26def IsTWitness (G : Graph α β) (T₁ T₂ : Set β) : Prop :=
    27 IsSpanningTree G T₁ ∧ IsSpanningTree G T₂ ∧ (T₁ ∩ T₂).encard ≤ 1
    28
    29/-- `G` is a `T`-graph: it has a `T`-witness. -/
    30def IsTGraph (G : Graph α β) : Prop :=
    31 ∃ T₁ T₂ : Set β, IsTWitness G T₁ T₂
    32
    33end Lax630294.TGraph
    34
    Formalization notes

    The two trees are given by their edge sets T1T₁ and T2T₂; they may coincide only when they have at most one edge in common, that is, when GG has at most two vertices.

    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…