Lax Lean Archive

Cubic graphs

Lax881656.Cubic · concepts/Lax881656/Cubic.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 cubic, or 3-regular, when every vertex has exactly three neighbors.

    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.Finite
    2import Mathlib.Data.Set.Card
    3
    4/-!
    5---
    6title: Cubic graphs
    7type: definition
    8---
    9A finite simple graph is cubic, or 3-regular, when every vertex has exactly
    10three neighbors.
    11
    12# Formalization notes
    13
    14The degree of a vertex is expressed as the cardinality of its neighbor set.
    15The ambient vertex type is finite, so these cardinalities are ordinary natural
    16numbers. No regularity data is carried beyond the pointwise condition.
    17-/
    18
    19set_option autoImplicit false
    20
    21namespace Lax881656.Cubic
    22
    23/-- A finite simple graph is cubic when every vertex has degree three. -/
    24def IsCubic {V : Type*} [Fintype V] (G : SimpleGraph V) : Prop :=
    25 ∀ v : V, (G.neighborSet v).ncard = 3
    26
    27end Lax881656.Cubic
    28
    Formalization notes

    The degree of a vertex is expressed as the cardinality of its neighbor set. The ambient vertex type is finite, so these cardinalities are ordinary natural numbers. No regularity data is carried beyond the pointwise condition.

    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…