Lax Lean Archive

Stars

Lax68.Stars · concepts/Lax68/Stars.lean · lax-68

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

    Star graph illustration
    Star graph illustration

    A star has a centre adjacent to every other vertex and has no edges between two non-central vertices.

    Concept map
    1 concept; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.UniversalVerts
    2
    3/-!
    4---
    5title: Stars
    6type: definition
    7---
    8
    9![Star graph illustration](https://raw.githubusercontent.com/lax-archive/lax-submissions/4dd917c8b9a1e181ec951b7f6fa384262af31fa9/planar-graph-classes-v4-33/assets/star.svg "Star graph illustration")
    10
    11A star has a centre adjacent to every other vertex and has no edges between
    12two non-central vertices.
    13-/
    14
    15set_option autoImplicit false
    16
    17namespace Lax68.Stars
    18
    19def HasStarShape {V : Type*} (G : SimpleGraph V) : Prop :=
    20 ∃ centre : V,
    21 centre ∈ G.universalVerts ∧
    22 ∀ ⦃u v⦄, G.Adj u v → u = centre ∨ v = centre
    23
    24def IsStar {V : Type*} (G : SimpleGraph V) : Prop :=
    25 HasStarShape G
    26
    27end Lax68.Stars
    28
    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…