Lax Lean Archive

3-connected graphs

Lax881656.ThreeConnected · concepts/Lax881656/ThreeConnected.lean · lax-881656

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 finite simple graph is 3-connected when it has at least four vertices and remains connected after deleting any set of at most two vertices.

    Concept map
    1 concept; 1 descendant hidden
    100%
    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
    2
    3/-!
    4---
    5title: 3-connected graphs
    6type: definition
    7---
    8A finite simple graph is 3-connected when it has at least four vertices and
    9remains connected after deleting any set of at most two vertices.
    10
    11# Formalization notes
    12
    13Deleting a finite set `S` is represented by the induced graph on the subtype
    14of vertices outside `S`. The cardinality condition rules out the small graphs
    15for which deletion-connectivity alone would make the usual definition
    16degenerate.
    17-/
    18
    19set_option autoImplicit false
    20
    21namespace Lax881656.ThreeConnected
    22
    23/-- A finite graph is 3-connected if deleting at most two vertices leaves a
    24connected graph, and the original graph has at least four vertices. -/
    25def IsThreeConnected {V : Type*} [Fintype V] [DecidableEq V]
    26 (G : SimpleGraph V) : Prop :=
    27 4 ≤ Fintype.card V ∧
    28 ∀ S : Finset V, S.card ≤ 2 →
    29 (G.induce {v : V | v ∉ S}).Connected
    30
    31end Lax881656.ThreeConnected
    32
    Formalization notes

    Deleting a finite set SS is represented by the induced graph on the subtype of vertices outside SS. The cardinality condition rules out the small graphs for which deletion-connectivity alone would make the usual definition degenerate.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…