Lax Lean Archive

Graph minors

Lax68.GraphMinors · concepts/Lax68/GraphMinors.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

    Graph minor illustration
    Graph minor illustration

    A graph H is a minor of a graph G when the vertices of H can be represented by pairwise disjoint connected branch sets in G, with an edge joining the corresponding branch sets for every edge of H.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    In the paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
    2
    3/-!
    4---
    5title: Graph minors
    6type: definition
    7---
    8
    9![Graph minor illustration](https://raw.githubusercontent.com/lax-archive/lax-submissions/4dd917c8b9a1e181ec951b7f6fa384262af31fa9/planar-graph-classes-v4-33/assets/graph-minor.svg "Graph minor illustration")
    10
    11A graph *H* is a minor of a graph *G* when the vertices of *H* can be
    12represented by pairwise disjoint connected branch sets in *G*, with an edge
    13joining the corresponding branch sets for every edge of *H*.
    14-/
    15
    16set_option autoImplicit false
    17
    18namespace Lax68.GraphMinors
    19
    20structure MinorModel {W V : Type*}
    21 (H : SimpleGraph W) (G : SimpleGraph V) where
    22 branchSet : W → Set V
    23 connected : ∀ w, (G.induce (branchSet w)).Connected
    24 disjoint :
    25 ∀ {u v}, u ≠ v →
    26 Disjoint (branchSet u) (branchSet v)
    27 adjacent :
    28 ∀ {u v}, H.Adj u v →
    29 ∃ x ∈ branchSet u, ∃ y ∈ branchSet v, G.Adj x y
    30
    31def IsMinor {W V : Type*}
    32 (H : SimpleGraph W) (G : SimpleGraph V) : Prop :=
    33 Nonempty (MinorModel H G)
    34
    35abbrev K5 : SimpleGraph (Fin 5) :=
    36 SimpleGraph.completeGraph (Fin 5)
    37
    38abbrev K4 : SimpleGraph (Fin 4) :=
    39 SimpleGraph.completeGraph (Fin 4)
    40
    41abbrev K33 : SimpleGraph (Fin 3 ⊕ Fin 3) :=
    42 completeBipartiteGraph (Fin 3) (Fin 3)
    43
    44abbrev K23 : SimpleGraph (Fin 2 ⊕ Fin 3) :=
    45 completeBipartiteGraph (Fin 2) (Fin 3)
    46
    47end Lax68.GraphMinors
    48
    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…