Lax Lean Archive

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

Clique minors and the Hadwiger number

Lax342547.CliqueMinor · concepts/Lax342547/CliqueMinor.lean · lax-342547

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 KtK_t minor is a family of tt nonempty connected, pairwise disjoint branch sets, with an edge joining every two distinct branch sets. The Hadwiger number h(G)h(G) is the largest such tt for a finite graph.

    Concept map
    1 concept; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1/-
    2Adapted from OpenAI, openai/math, commit
    3adc7f1241b42e322a6451854ab7e4b4c146bf78a (Apache-2.0).
    4Changes: Lax package separation, namespaces, explicit variables, and archive annotations.
    5-/
    6import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
    7import Mathlib.Order.Lattice.Nat
    8
    9/-!
    10---
    11title: Clique minors and the Hadwiger number
    12type: definition
    13---
    14A KtK_t minor is a family of tt nonempty connected, pairwise disjoint branch
    15sets, with an edge joining every two distinct branch sets. The Hadwiger
    16number h(G)h(G) is the largest such tt for a finite graph.
    17-/
    18
    19namespace Lax342547.CliqueMinor
    20
    21def HasCliqueMinor {V : Type} (G : SimpleGraph V) (t : ℕ) : Prop :=
    22 ∃ B : Fin t → Set V,
    23 (∀ i, (G.induce (B i)).Connected) ∧
    24 (∀ i j, i ≠ j → Disjoint (B i) (B j)) ∧
    25 (∀ i j, i ≠ j → ∃ v ∈ B i, ∃ w ∈ B j, G.Adj v w)
    26
    27noncomputable def hadwigerNumber {V : Type} (G : SimpleGraph V) : ℕ :=
    28 sSup {t : ℕ | HasCliqueMinor G t}
    29
    30
    31end Lax342547.CliqueMinor
    32
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…