Lax Lean Archive

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

Distance to cluster graphs

Lax825442.DistanceToCluster · concepts/Lax825442/DistanceToCluster.lean · lax-825442

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 cluster graph is a disjoint union of cliques, including isolated vertices and the empty graph. Equivalently, its complement is complete multipartite. The distance to cluster graphs is the minimum number of vertices whose deletion leaves a cluster induced graph. The target predicate reuses mathlib's SimpleGraph.IsCompleteMultipartiteSimpleGraph.IsCompleteMultipartite on the complement.

    Concept map
    1 concept
    100%
    DefinitionThis concept

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
    2import Mathlib.Combinatorics.SimpleGraph.Finite
    3import Mathlib.Order.Lattice.Nat
    4
    5/-!
    6---
    7title: Distance to cluster graphs
    8type: definition
    9---
    10A cluster graph is a disjoint union of cliques, including isolated vertices
    11and the empty graph. Equivalently, its complement is complete multipartite.
    12The distance to cluster graphs is the minimum number of vertices whose
    13deletion leaves a cluster induced graph. The target predicate reuses
    14mathlib's `SimpleGraph.IsCompleteMultipartite` on the complement.
    15-/
    16
    17namespace Lax825442.DistanceToCluster
    18
    19/-- Minimum number of vertices whose deletion leaves a disjoint union of cliques. -/
    20noncomputable def distanceToCluster {V : Type} [Fintype V] [DecidableEq V]
    21 (G : SimpleGraph V) : ℕ :=
    22 sInf {k : ℕ | ∃ S : Finset V, (S.card = k) ∧
    23 ((G.induce {v | v ∉ S})ᶜ.IsCompleteMultipartite)}
    24
    25end Lax825442.DistanceToCluster
    26
    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…