Lax Lean Archive

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

The chromatic lower bound for independence number two

Lax342547.ChromaticBound · concepts/Lax342547/ChromaticBound.lean · lax-342547

proven

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

    Theorem

    A finite graph of independence number at most two satisfies ∣V(G)∣≤2χ(G)|V(G)|\le 2\chi(G), since every color class has at most two vertices.

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
    2
    3/-!
    4---
    5title: The chromatic lower bound for independence number two
    6type: theorem
    7---
    8A finite graph of independence number at most two satisfies
    9∣V(G)∣≤2χ(G)|V(G)|\le 2\chi(G), since every color class has at most two vertices.
    10-/
    11
    12namespace Lax342547.ChromaticBound
    13
    14axiom card_le_twice_chromaticNumber_of_indepNum
    15 {V : Type*} [Fintype V] (G : SimpleGraph V) (hα : G.indepNum ≤ 2) :
    16 Fintype.card V ≤ 2 * G.chromaticNumber.toNat
    17
    18end Lax342547.ChromaticBound
    19
    Show Proof
    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…