Lax Lean Archive

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

Edge clique cover number

Lax560391.EdgeCliqueCover · concepts/Lax560391/EdgeCliqueCover.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

    An edge clique cover is a family of vertex cliques such that every graph edge has both endpoints in at least one family member. Its number is the minimum size of such a family. An edgeless graph has edge clique cover number zero.

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

    Lean source view on GitHub

    1import Lax560391.EdgeCliqueCovering
    2import Mathlib.Order.Lattice.Nat
    3
    4/-!
    5---
    6title: Edge clique cover number
    7type: definition
    8---
    9An edge clique cover is a family of vertex cliques such that every graph edge
    10has both endpoints in at least one family member. Its number is the minimum
    11size of such a family. An edgeless graph has edge clique cover number zero.
    12-/
    13
    14namespace Lax560391.EdgeCliqueCover
    15
    16/-- `k` indexed cliques cover every edge of `G`. Repeated or empty cliques
    17are harmless because the minimum index count is taken. -/
    18def HasEdgeCliqueCoverAtMost {V : Type} [DecidableEq V]
    19 (G : SimpleGraph V) (k : ℕ) : Prop :=
    20 Nonempty (Lax560391.EdgeCliqueCovering.EdgeCliqueCovering G k)
    21
    22noncomputable def edgeCliqueCover {V : Type} [Fintype V] [DecidableEq V]
    23 (G : SimpleGraph V) : ℕ :=
    24 sInf {k | HasEdgeCliqueCoverAtMost G k}
    25
    26end Lax560391.EdgeCliqueCover
    27
    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…