Labeled directed graphs

StructureLabeled directed graph#✓fully proved

A labeled directed graph with vertex set \(V\), edge set \(E\) and label set \(L\) consists of a source map \(s : E \to V\), a target map \(t : E \to V\) and a label map \(\ell : E \to L\); the edge \(e\) goes from \(s(e)\) to \(t(e)\) and carries the label \(\ell(e)\). Loops and parallel edges are allowed.

structure LabeledDigraph (V E L : Type _) where
  src : E → V
  tgt : E → V
  label : E → L

Used by 9

Used byExtensionality for labeled directed graphs · Restriction of a labeled directed graph · Label of an edge in a restriction · Source of an edge in a restriction · Target of an edge in a restriction · Young graph of a labeled directed graph · Label of an edge in the Young graph · Source of an edge in the Young graph · Target of an edge in the Young graph

TheoremExtensionality for labeled directed graphs#✓fully proved

Two labeled directed graphs \(G\) and \(H\) with the same vertex set, edge set and label set are equal if they have the same source map, the same target map and the same label map.

@[ext]
theorem LabeledDigraph.ext {V E L : Type _} {G H : LabeledDigraph V E L}
    (hsrc : G.src = H.src) (htgt : G.tgt = H.tgt) (hlabel : G.label = H.label) :
    G = H

Uses 1

Statement usesLabeled directed graph

DefinitionRestriction of a labeled directed graph#✓fully proved

Let \(G\) be a labeled directed graph with vertex set \(V\) and label set \(L\), and let \(p\) be a predicate on \(V\). The restriction of \(G\) to \(p\) is the labeled directed graph with label set \(L\) whose vertices are the vertices \(v\) of \(G\) with \(p(v)\), whose edges are the edges of \(G\) whose source and target both satisfy \(p\), and in which each edge has the same source, target and label as in \(G\).

def LabeledDigraph.restrict {V E L : Type _} (G : LabeledDigraph V E L)
    (p : V → Prop) :
    LabeledDigraph { v : V // p v } { e : E // p (G.src e) ∧ p (G.tgt e) } L where
  src e := ⟨G.src e.val, e.property.1⟩
  tgt e := ⟨G.tgt e.val, e.property.2⟩
  label e := G.label e.val

Uses 1 · Used by 4

Statement usesLabeled directed graph

Used byLabel of an edge in a restriction · Source of an edge in a restriction · Target of an edge in a restriction · Young graph of a labeled directed graph

TheoremSource of an edge in a restriction#✓fully proved

Let \(G\) be a labeled directed graph, \(p\) a predicate on its vertices, and \(e\) an edge of \(G\) whose source and target satisfy \(p\), viewed as an edge of the restriction of \(G\) to \(p\). The source of \(e\) in the restriction, viewed as a vertex of \(G\), is the source of \(e\) in \(G\).

@[simp]
theorem LabeledDigraph.restrict_src {V E L : Type _} (G : LabeledDigraph V E L)
    (p : V → Prop) (e : { e : E // p (G.src e) ∧ p (G.tgt e) }) :
    ((G.restrict p).src e).val = G.src e.val

Uses 2

Statement usesLabeled directed graph · Restriction of a labeled directed graph

TheoremTarget of an edge in a restriction#✓fully proved

Let \(G\) be a labeled directed graph, \(p\) a predicate on its vertices, and \(e\) an edge of \(G\) whose source and target satisfy \(p\), viewed as an edge of the restriction of \(G\) to \(p\). The target of \(e\) in the restriction, viewed as a vertex of \(G\), is the target of \(e\) in \(G\).

@[simp]
theorem LabeledDigraph.restrict_tgt {V E L : Type _} (G : LabeledDigraph V E L)
    (p : V → Prop) (e : { e : E // p (G.src e) ∧ p (G.tgt e) }) :
    ((G.restrict p).tgt e).val = G.tgt e.val

Uses 2

Statement usesLabeled directed graph · Restriction of a labeled directed graph

TheoremLabel of an edge in a restriction#✓fully proved

Let \(G\) be a labeled directed graph, \(p\) a predicate on its vertices, and \(e\) an edge of \(G\) whose source and target satisfy \(p\), viewed as an edge of the restriction of \(G\) to \(p\). The label of \(e\) in the restriction is its label in \(G\).

@[simp]
theorem LabeledDigraph.restrict_label {V E L : Type _} (G : LabeledDigraph V E L)
    (p : V → Prop) (e : { e : E // p (G.src e) ∧ p (G.tgt e) }) :
    (G.restrict p).label e = G.label e.val

Uses 2

Statement usesLabeled directed graph · Restriction of a labeled directed graph

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.