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 #
-
Subgraph G
is the type of subgraphs of aG : SimpleGraph V
. -
Subgraph.neighborSet
,Subgraph.incidenceSet
, andSubgraph.degree
are like theirSimpleGraph
counterparts, but they refer to vertices fromG
to avoid subtype coercions. -
Subgraph.coe
is the coercion from aG' : Subgraph G
to aSimpleGraph G'.verts
. (In Lean 3 this could not be aCoe
instance since the destination type depends onG'
.) -
Subgraph.IsSpanning
for whether a subgraph is a spanning subgraph andSubgraph.IsInduced
for whether a subgraph is an induced subgraph. -
Instances for
Lattice (Subgraph G)
andBoundedOrder (Subgraph G)
. -
SimpleGraph.toSubgraph
: If aSimpleGraph
is a subgraph of another, then you can turn it into a member of the larger graph'sSimpleGraph.Subgraph
type. -
Graph homomorphisms from a subgraph to a graph (
Subgraph.map_top
) and between subgraphs (Subgraph.map
).
Implementation notes #
- Recall that subgraphs are not determined by their vertex sets, so
SetLike
does not apply to this kind of subobject.
Todo #
- Images of graph homomorphisms as subgraphs.
- verts : Set V
- Adj : V → V → Prop
- adj_sub : ∀ {v w : V}, SimpleGraph.Subgraph.Adj s v w → SimpleGraph.Adj G v w
- edge_vert : ∀ {v w : V}, SimpleGraph.Subgraph.Adj s v w → v ∈ s.verts
- symm : Symmetric s.Adj
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.
Thinking of V → V → Prop
as Set (V × V)
, a set of darts (i.e., half-edges), then
Subgraph.adj_sub
is that the darts of a subgraph are a subset of the darts of G
.
Instances For
The one-vertex subgraph.
Instances For
The one-edge subgraph.
Instances For
Coercion from G' : Subgraph G
to a SimpleGraph G'.verts
.
Instances For
A subgraph is called a spanning subgraph if it contains all the vertices of G
.
Instances For
Coercion from Subgraph G
to SimpleGraph V
. If G'
is a spanning
subgraph, then G'.spanningCoe
yields an isomorphic graph.
In general, this adds in all vertices from V
as isolated vertices.
Instances For
spanningCoe
is equivalent to coe
for a subgraph that IsSpanning
.
Instances For
A subgraph is called an induced subgraph if vertices of G'
are adjacent if
they are adjacent in G
.
Instances For
H.support
is the set of vertices that form edges in the subgraph H
.
Instances For
G'.neighborSet v
is the set of vertices adjacent to v
in G'
.
Instances For
A subgraph as a graph has equivalent neighbor sets.
Instances For
The edge set of G'
consists of a subset of edges of G
.
Instances For
The incidenceSet
is the set of edges incident to a given vertex.
Instances For
Give a vertex as an element of the subgraph's vertex type.
Instances For
Create an equal copy of a subgraph (see copy_eq
) with possibly different definitional equalities.
See Note [range copy pattern].
Instances For
The union of two subgraphs.
The intersection of two subgraphs.
The top
subgraph is G
as a subgraph of itself.
The bot
subgraph is the subgraph with no vertices or edges.
For subgraphs G₁
, G₂
, G₁ ≤ G₂
iff G₁.verts ⊆ G₂.verts
and
∀ a b, G₁.adj a b → G₂.adj a b
.
Turn a subgraph of a SimpleGraph
into a member of its subgraph type.
Instances For
The top of the Subgraph G
lattice is equivalent to the graph itself.
Instances For
The bottom of the Subgraph G
lattice is equivalent to the empty graph on the empty
vertex type.
Instances For
Graph homomorphisms induce a covariant function on subgraphs.
Instances For
Graph homomorphisms induce a contravariant function on subgraphs.
Instances For
Given two subgraphs, one a subgraph of the other, there is an induced injective homomorphism of the subgraphs as graphs.
Instances For
There is an induced injective homomorphism of a subgraph of G
into G
.
Instances For
There is an induced injective homomorphism of a subgraph of G
as
a spanning subgraph into G
.
Instances For
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.
Instances For
The degree of a vertex in a subgraph. It's zero for vertices outside the subgraph.
Instances For
Properties of singletonSubgraph
and subgraphOfAdj
#
Subgraphs of subgraphs #
Given a subgraph of a subgraph of G
, construct a subgraph of G
.
Instances For
Given a subgraph of G
, restrict it to being a subgraph of another subgraph G'
by
taking the portion of G
that intersects G'
.
Instances For
Edge deletion #
Given a subgraph G'
and a set of vertex pairs, remove all of the corresponding edges
from its edge set, if present.
See also: SimpleGraph.deleteEdges
.
Instances For
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 G'
.
Instances For
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.