Lax Lean Archive

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

Vertex integrity

Lax560391.VertexIntegrity · concepts/Lax560391/VertexIntegrity.lean · lax-560391

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

    The vertex integrity of a finite graph is the minimum, over vertex sets SS, of the size of SS plus the order of the largest connected component of the graph induced by the remaining vertices. The maximum component order is zero when no vertices remain.

    Concept map
    1 concept
    100%
    DefinitionThis concept

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
    2import Mathlib.Data.Set.Card
    3import Mathlib.Order.Lattice.Nat
    4
    5/-!
    6---
    7title: Vertex integrity
    8type: definition
    9---
    10The vertex integrity of a finite graph is the minimum, over vertex sets `S`,
    11of the size of `S` plus the order of the largest connected component of the
    12graph induced by the remaining vertices. The maximum component order is zero
    13when no vertices remain.
    14-/
    15
    16namespace Lax560391.VertexIntegrity
    17
    18/-- Deleting `S` leaves no component larger than `k - |S|`. -/
    19def HasVertexIntegrityAtMost {V : Type} [Fintype V] [DecidableEq V]
    20 (G : SimpleGraph V) (k : ℕ) : Prop :=
    21 ∃ S : Set V, S.ncard ≤ k ∧
    22 ∀ C : (G.induce Sᶜ).ConnectedComponent,
    23 S.ncard + C.supp.ncard ≤ k
    24
    25/-- The minimum of deletion-set size plus largest remaining component size. -/
    26noncomputable def vertexIntegrity {V : Type} [Fintype V] [DecidableEq V]
    27 (G : SimpleGraph V) : ℕ :=
    28 sInf {k | HasVertexIntegrityAtMost G k}
    29
    30end Lax560391.VertexIntegrity
    31
    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…