Lax Lean Archive

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

Twin-cover number

Lax825442.TwinCover · concepts/Lax825442/TwinCover.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 twin-cover meets every edge whose endpoints are not true twins in the original graph. The twin-cover number is the minimum cardinality of such a set.

    Concept map
    1 concept
    100%
    DefinitionThis concept

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Finite
    2import Mathlib.Data.Set.Card
    3import Mathlib.Order.Lattice.Nat
    4
    5/-!
    6---
    7title: Twin-cover number
    8type: definition
    9---
    10A twin-cover meets every edge whose endpoints are not true twins in the
    11original graph. The twin-cover number is the minimum cardinality of such a
    12set.
    13-/
    14
    15namespace Lax825442.TwinCover
    16
    17/-- Adjacent vertices with the same neighbors outside the pair. -/
    18def TrueTwins {V : Type} (G : SimpleGraph V) (u v : V) : Prop :=
    19 G.Adj u v ∧ (∀ w : V,
    20 (w ≠ u ∧ w ≠ v) → (G.Adj u w ↔ G.Adj v w))
    21
    22/-- A set meeting every edge except those between true twins. -/
    23def IsTwinCover {V : Type} (G : SimpleGraph V) (S : Set V) : Prop :=
    24 ∀ ⦃u v : V⦄,
    25 (G.Adj u v ∧ ¬ TrueTwins G u v) → (u ∈ S ∨ v ∈ S)
    26
    27/-- The minimum cardinality of a twin-cover. -/
    28noncomputable def twinCover {V : Type} [Fintype V] [DecidableEq V]
    29 (G : SimpleGraph V) : ℕ :=
    30 sInf {k | ∃ S : Set V, (S.ncard = k) ∧ IsTwinCover G S}
    31
    32end Lax825442.TwinCover
    33
    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…