Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax10.ThreeConnectedAndColorable

3-connected graphs and 4-colorability

concepts/Lax10/ThreeConnectedAndColorable.lean · lax-10

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    A graph is 33-connected when it has at least 4 vertices and remains connected after deleting any set of at most two vertices. A graph is mm-colorable when its vertices have a proper coloring with at most mm colors; in particular, 44-colorability is the case m=4m = 4.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
    2
    3/-!
    4---
    5title: 3-connected graphs and 4-colorability
    6type: definition
    7---
    8A graph is 33-connected when it has at least 4 vertices and remains
    9connected after deleting any set of at most two vertices. A graph is
    10mm-colorable when its vertices have a proper coloring with at most mm
    11colors; in particular, 44-colorability is the case m=4m = 4.
    12-/
    13
    14open Finset
    15
    16namespace Lax10.ThreeConnectedAndColorable
    17
    18universe u
    19
    20variable {V : Type u}
    21
    22/-- A simple graph is colorable with at most mm colors. -/
    23def KColorable (m : Nat) (G : SimpleGraph V) : Prop :=
    24 G.Colorable m
    25
    26/-- The induced graph obtained after deleting the vertices in SS. -/
    27def deleteVertices (G : SimpleGraph V) (S : Finset V) :
    28 SimpleGraph {v : V // v ∉ S} :=
    29 G.induce {v : V | v ∉ S}
    30
    31/-- The set SS separates two vertices that remain after its deletion. -/
    32def IsVertexSeparator (G : SimpleGraph V) (S : Finset V) : Prop :=
    33 ∃ x y : {v : V // v ∉ S}, ¬ (deleteVertices G S).Reachable x y
    34
    35/--
    36A graph is 33-connected when it has at least 4 vertices and no vertex
    37separator of size at most two.
    38-/
    39def ThreeConnected (G : SimpleGraph V) : Prop :=
    40 4 ≤ Nat.card V ∧
    41 ∀ S : Finset V, S.card ≤ 2 → ¬ IsVertexSeparator G S
    42
    43end Lax10.ThreeConnectedAndColorable
    44

    Builds on

    none

    Used by

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…