Documentation

Mathlib.Combinatorics.SimpleGraph.Dart

Darts in graphs #

A Dart or half-edge or bond in a graph is an ordered pair of adjacent vertices, regarded as an oriented edge. This file defines darts and proves some of their basic properties.

source
structure SimpleGraph.Dart {V : Type u_1} (G : SimpleGraph V) extends Prod :
Type u_1

A Dart is an oriented edge, implemented as an ordered pair of adjacent vertices. This terminology comes from combinatorial maps, and they are also known as "half-edges" or "bonds."

  • fst : V
  • snd : V
  • is_adj : G.Adj self.toProd.1 self.toProd.2
Instances For
    source
    instance SimpleGraph.instDecidableEqDart :
    {V : Type u_2} → {G : SimpleGraph V} → [inst : DecidableEq V] → DecidableEq (SimpleGraph.Dart G)
    Equations
    • SimpleGraph.instDecidableEqDart = SimpleGraph.decEqDart✝
    source
    theorem SimpleGraph.Dart.ext_iff {V : Type u_1} {G : SimpleGraph V} (d₁ : SimpleGraph.Dart G) (d₂ : SimpleGraph.Dart G) :
    d₁ = d₂ ↔ d₁.toProd = d₂.toProd
    source
    theorem SimpleGraph.Dart.ext {V : Type u_1} {G : SimpleGraph V} (d₁ : SimpleGraph.Dart G) (d₂ : SimpleGraph.Dart G) (h : d₁.toProd = d₂.toProd) :
    d₁ = d₂
    source
    theorem SimpleGraph.Dart.toProd_injective {V : Type u_1} {G : SimpleGraph V} :
    Function.Injective SimpleGraph.Dart.toProd
    source
    instance SimpleGraph.Dart.fintype {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] :
    Fintype (SimpleGraph.Dart G)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def SimpleGraph.Dart.edge {V : Type u_1} {G : SimpleGraph V} (d : SimpleGraph.Dart G) :
    Sym2 V

    The edge associated to the dart.

    Equations
    Instances For
      source
      @[simp]
      theorem SimpleGraph.Dart.edge_mk {V : Type u_1} {G : SimpleGraph V} {p : V × V} (h : G.Adj p.1 p.2) :
      SimpleGraph.Dart.edge { toProd := p, is_adj := h } = Sym2.mk p
      source
      @[simp]
      theorem SimpleGraph.Dart.edge_mem {V : Type u_1} {G : SimpleGraph V} (d : SimpleGraph.Dart G) :
      SimpleGraph.Dart.edge d ∈ SimpleGraph.edgeSet G
      source
      @[simp]
      theorem SimpleGraph.Dart.symm_toProd {V : Type u_1} {G : SimpleGraph V} (d : SimpleGraph.Dart G) :
      (SimpleGraph.Dart.symm d).toProd = Prod.swap d.toProd
      source
      def SimpleGraph.Dart.symm {V : Type u_1} {G : SimpleGraph V} (d : SimpleGraph.Dart G) :
      SimpleGraph.Dart G

      The dart with reversed orientation from a given dart.

      Equations
      Instances For
        source
        @[simp]
        theorem SimpleGraph.Dart.symm_mk {V : Type u_1} {G : SimpleGraph V} {p : V × V} (h : G.Adj p.1 p.2) :
        SimpleGraph.Dart.symm { toProd := p, is_adj := h } = { toProd := Prod.swap p, is_adj := (_ : G.Adj p.2 p.1) }
        source
        @[simp]
        theorem SimpleGraph.Dart.edge_symm {V : Type u_1} {G : SimpleGraph V} (d : SimpleGraph.Dart G) :
        SimpleGraph.Dart.edge (SimpleGraph.Dart.symm d) = SimpleGraph.Dart.edge d
        source
        @[simp]
        theorem SimpleGraph.Dart.edge_comp_symm {V : Type u_1} {G : SimpleGraph V} :
        SimpleGraph.Dart.edge ∘ SimpleGraph.Dart.symm = SimpleGraph.Dart.edge
        source
        @[simp]
        theorem SimpleGraph.Dart.symm_symm {V : Type u_1} {G : SimpleGraph V} (d : SimpleGraph.Dart G) :
        SimpleGraph.Dart.symm (SimpleGraph.Dart.symm d) = d
        source
        @[simp]
        theorem SimpleGraph.Dart.symm_involutive {V : Type u_1} {G : SimpleGraph V} :
        Function.Involutive SimpleGraph.Dart.symm
        source
        theorem SimpleGraph.Dart.symm_ne {V : Type u_1} {G : SimpleGraph V} (d : SimpleGraph.Dart G) :
        SimpleGraph.Dart.symm d ≠ d
        source
        theorem SimpleGraph.dart_edge_eq_iff {V : Type u_1} {G : SimpleGraph V} (d₁ : SimpleGraph.Dart G) (d₂ : SimpleGraph.Dart G) :
        SimpleGraph.Dart.edge d₁ = SimpleGraph.Dart.edge d₂ ↔ d₁ = d₂ ∨ d₁ = SimpleGraph.Dart.symm d₂
        source
        theorem SimpleGraph.dart_edge_eq_mk'_iff {V : Type u_1} {G : SimpleGraph V} {d : SimpleGraph.Dart G} {p : V × V} :
        SimpleGraph.Dart.edge d = Sym2.mk p ↔ d.toProd = p ∨ d.toProd = Prod.swap p
        source
        theorem SimpleGraph.dart_edge_eq_mk'_iff' {V : Type u_1} {G : SimpleGraph V} {d : SimpleGraph.Dart G} {u : V} {v : V} :
        SimpleGraph.Dart.edge d = s(u, v) ↔ d.toProd.1 = u ∧ d.toProd.2 = v ∨ d.toProd.1 = v ∧ d.toProd.2 = u
        source
        def SimpleGraph.DartAdj {V : Type u_1} (G : SimpleGraph V) (d : SimpleGraph.Dart G) (d' : SimpleGraph.Dart G) :
        Prop

        Two darts are said to be adjacent if they could be consecutive darts in a walk -- that is, the first dart's second vertex is equal to the second dart's first vertex.

        Equations
        Instances For
          source
          @[simp]
          theorem SimpleGraph.dartOfNeighborSet_toProd {V : Type u_1} (G : SimpleGraph V) (v : V) (w : ↑(SimpleGraph.neighborSet G v)) :
          (SimpleGraph.dartOfNeighborSet G v w).toProd = (v, ↑w)
          source
          def SimpleGraph.dartOfNeighborSet {V : Type u_1} (G : SimpleGraph V) (v : V) (w : ↑(SimpleGraph.neighborSet G v)) :
          SimpleGraph.Dart G

          For a given vertex v, this is the bijective map from the neighbor set at v to the darts d with d.fst = v.

          Equations
          Instances For
            source
            theorem SimpleGraph.dartOfNeighborSet_injective {V : Type u_1} (G : SimpleGraph V) (v : V) :
            Function.Injective (SimpleGraph.dartOfNeighborSet G v)
            source
            instance SimpleGraph.nonempty_dart_top {V : Type u_1} [Nontrivial V] :
            Nonempty (SimpleGraph.Dart ⊤)
            Equations