Subgraphs of a simple graph #
A subgraph of a simple graph consists of subsets of the graph's vertices and edges such that the endpoints of each edge are present in the vertex subset. The edge subset is formalized as a sub-relation of the adjacency relation of the simple graph.
Main definitions #
Graph homomorphisms from a subgraph to a graph (
Subgraph.map_top) and between subgraphs (
Implementation notes #
- Recall that subgraphs are not determined by their vertex sets, so
SetLikedoes not apply to this kind of subobject.
- Images of graph homomorphisms as subgraphs.
A subgraph of a
SimpleGraph is a subset of vertices along with a restriction of the adjacency
relation that is symmetric and is supported by the vertex subset. They also form a bounded lattice.
Create an equal copy of a subgraph (see
copy_eq) with possibly different definitional equalities.
See Note [range copy pattern].
Given two subgraphs, one a subgraph of the other, there is an induced injective homomorphism of the subgraphs as graphs.
If a graph is locally finite at a vertex, then so is a subgraph of that graph.
If a subgraph is locally finite at a vertex, then so are subgraphs of that subgraph.
This is not an instance because
G'' cannot be inferred.
Subgraphs of subgraphs #
Given a subgraph of
G, restrict it to being a subgraph of another subgraph
taking the portion of
G that intersects
Edge deletion #
Given a subgraph
G' and a set of vertex pairs, remove all of the corresponding edges
from its edge set, if present.
Induced subgraphs #
The induced subgraph of a subgraph. The expectation is that
s ⊆ G'.verts for the usual
notion of an induced subgraph, but, in general,
s is taken to be the new vertex set and edges
are induced from the subgraph
Given a subgraph and a set of vertices, delete all the vertices from the subgraph, if present. Any edges incident to the deleted vertices are deleted as well.