How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Degree in a multigraph, indegree and outdegree in a digraph, and their underlying connectivity
Definition
Let be a finite undirected multigraph (Multigraphs, loops and directed graphs as variants distinct from the default finite simple graph). The degree of a vertex is the number of incident edge ends: each nonloop edge incident with contributes one, and each loop at contributes two.
For a finite digraph , the outdegree and indegree are
A directed loop contributes one to each quantity. A digraph vertex is isolated when both degrees are zero. A multigraph vertex is isolated when its degree is zero.
The underlying undirected graph of a multigraph is obtained by deleting loops and replacing each nonempty parallel class by one simple edge. The underlying undirected graph of a digraph has an edge for distinct whenever or is an arc. A multigraph or digraph is weakly connected when this underlying graph is connected in the sense of Connected graphs and connected components defined by the existence of vertex paths. Thus the null graph is not weakly connected and a one-vertex underlying graph is connected.
These finite counts use The cardinality of a finite set, and the underlying objects use the simple-graph convention of A finite simple graph is a finite vertex set together with a set of two-element vertex subsets.
Depends on
- Multigraphs, loops and directed graphs as variants distinct from the default finite simple graph
- The cardinality $\lvert A\rvert$ of a finite set
- A finite simple graph is a finite vertex set together with a set of two-element vertex subsets
- Connected graphs and connected components defined by the existence of vertex paths
Used by
- A connected finite undirected multigraph has an Euler trail if and only if it has zero or two odd-degree vertices; an open Euler trail occurs exactly in the two-vertex case Corollary
- Directed walks, trails, paths and cycles, and strong connectivity Definition
- The Konigsberg bridges multigraph has four odd-degree vertices and no Euler trail Example
- In an even multigraph or balanced digraph, a trail maximal among unused incident edges returns to its start Lemma
- A finite digraph without isolated vertices has a directed Euler circuit if and only if it is weakly connected and every indegree equals the corresponding outdegree Theorem
- Euler's theorem and Hierholzer's construction: a connected finite undirected multigraph has an Euler circuit if and only if every degree is even Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 32 results over 16 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Applied Combinatorics, Euler Tours and Trails (standard reference, not scraped)
- Applied Combinatorics, Directed Graphs (standard reference, not scraped)