Lax Lean Archive

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

Distance to cographs

Lax825442.DistanceToCograph · concepts/Lax825442/DistanceToCograph.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

    The distance to cographs is the minimum number of vertices whose deletion leaves a cograph. The remaining graph is induced on the vertices outside the deleted set. Cograph membership uses the registered Lax214022.Cographs.IsCographLax214022.Cographs.IsCograph, expressed through a twin-width-zero contraction sequence. This is the standard cograph class, equivalently the graphs with no induced four-vertex path.

    Concept map
    3 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax214022.Cographs
    2import Mathlib.Combinatorics.SimpleGraph.Finite
    3import Mathlib.Order.Lattice.Nat
    4
    5/-!
    6---
    7title: Distance to cographs
    8type: definition
    9---
    10The distance to cographs is the minimum number of vertices whose deletion
    11leaves a cograph. The remaining graph is induced on the vertices outside the
    12deleted set. Cograph membership uses the registered `Lax214022.Cographs.IsCograph`,
    13expressed through a twin-width-zero contraction sequence. This is the standard
    14cograph class, equivalently the graphs with no induced four-vertex path.
    15-/
    16
    17namespace Lax825442.DistanceToCograph
    18
    19/-- Minimum number of vertices whose deletion leaves a cograph. -/
    20noncomputable def distanceToCograph {V : Type} [Fintype V] [DecidableEq V]
    21 (G : SimpleGraph V) : ℕ :=
    22 sInf {k : ℕ | ∃ S : Finset V, (S.card = k) ∧
    23 (Lax214022.Cographs.IsCograph (G.induce {v | v ∉ S}))}
    24
    25end Lax825442.DistanceToCograph
    26
    Builds on
    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…