Lax Lean Archive

Asteroidal triples of cycles

Lax762056.AsteroidalCycles · concepts/Lax762056/AsteroidalCycles.lean · lax-762056

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

    An asteroidal triple of cycles consists of three vertex-disjoint, pairwise nonadjacent cycles such that every pair is joined by a path avoiding the closed neighborhood of the third.

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

    In the paper

    • page 5 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Paths
    2
    3/-!
    4---
    5title: Asteroidal triples of cycles
    6type: definition
    7---
    8An asteroidal triple of cycles consists of three vertex-disjoint, pairwise
    9nonadjacent cycles such that every pair is joined by a path avoiding the
    10closed neighborhood of the third.
    11-/
    12
    13namespace Lax762056.AsteroidalCycles
    14
    15open SimpleGraph
    16
    17def AvoidsClosedNeighborhood {V : Type*} (G : SimpleGraph V)
    18 (S T : Set V) : Prop :=
    19 ∀ x ∈ S, ∀ y ∈ T, x ≠ y ∧ ¬ G.Adj x y
    20
    21def HasAsteroidalCycleTriple {V : Type*} (G : SimpleGraph V) : Prop :=
    22 ∃ (base : Fin 3 → V) (cycle : ∀ i, Walk G (base i) (base i)),
    23 (∀ i, (cycle i).IsCycle) ∧
    24 (Pairwise fun i j => AvoidsClosedNeighborhood G
    25 {v | v ∈ (cycle i).support} {v | v ∈ (cycle j).support}) ∧
    26 (∀ i j k, i ≠ j → i ≠ k → j ≠ k →
    27 ∃ u ∈ (cycle i).support, ∃ v ∈ (cycle j).support,
    28 ∃ p : Path G u v, AvoidsClosedNeighborhood G
    29 {x | x ∈ p.val.support} {x | x ∈ (cycle k).support})
    30
    31end Lax762056.AsteroidalCycles
    32
    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…