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 a G : SimpleGraph V.

• Subgraph.neighborSet, Subgraph.incidenceSet, and Subgraph.degree are like their SimpleGraph counterparts, but they refer to vertices from G to avoid subtype coercions.

• Subgraph.coe is the coercion from a G' : Subgraph G to a SimpleGraph G'.verts. (In Lean 3 this could not be a Coe instance since the destination type depends on G'.)

• Subgraph.IsSpanning for whether a subgraph is a spanning subgraph and Subgraph.IsInduced for whether a subgraph is an induced subgraph.

• Instances for Lattice (Subgraph G) and BoundedOrder (Subgraph G).

• SimpleGraph.toSubgraph: If a SimpleGraph is a subgraph of another, then you can turn it into a member of the larger graph's SimpleGraph.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.

theorem SimpleGraph.Subgraph.ext {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) (y : SimpleGraph.Subgraph G) (verts : x.verts = y.verts) (Adj : x.Adj = y.Adj) : x = y

theorem SimpleGraph.Subgraph.ext_iff {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) (y : SimpleGraph.Subgraph G) : x = y ↔ x.verts = y.verts ∧ x.Adj = y.Adj

structure SimpleGraph.Subgraph {V : Type u} (G : SimpleGraph V) : Type u

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.

• verts : Set V
• Adj : V → V → Prop
• adj_sub : ∀ {v w : V}, self.Adj v w → G.Adj v w
• edge_vert : ∀ {v w : V}, self.Adj v w → v ∈ self.verts
• symm : Symmetric self.Adj

@[simp]

theorem SimpleGraph.singletonSubgraph_adj {V : Type u} (G : SimpleGraph V) (v : V) : ∀ (a a_1 : V), (SimpleGraph.singletonSubgraph G v).Adj a a_1 = ⊥ a a_1

@[simp]

theorem SimpleGraph.singletonSubgraph_verts {V : Type u} (G : SimpleGraph V) (v : V) : (SimpleGraph.singletonSubgraph G v).verts = {v}

def SimpleGraph.singletonSubgraph {V : Type u} (G : SimpleGraph V) (v : V) : SimpleGraph.Subgraph G

The one-vertex subgraph.

Equations

• SimpleGraph.singletonSubgraph G v = { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

@[simp]

theorem SimpleGraph.subgraphOfAdj_adj {V : Type u} (G : SimpleGraph V) {v : V} {w : V} (hvw : G.Adj v w) (a : V) (b : V) : (SimpleGraph.subgraphOfAdj G hvw).Adj a b = (s(v, w) = s(a, b))

@[simp]

theorem SimpleGraph.subgraphOfAdj_verts {V : Type u} (G : SimpleGraph V) {v : V} {w : V} (hvw : G.Adj v w) : (SimpleGraph.subgraphOfAdj G hvw).verts = {v, w}

def SimpleGraph.subgraphOfAdj {V : Type u} (G : SimpleGraph V) {v : V} {w : V} (hvw : G.Adj v w) : SimpleGraph.Subgraph G

The one-edge subgraph.

Equations

• SimpleGraph.subgraphOfAdj G hvw = { verts := {v, w}, Adj := fun (a b : V) => s(v, w) = s(a, b), adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

theorem SimpleGraph.Subgraph.loopless {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) : Irreflexive G'.Adj

theorem SimpleGraph.Subgraph.adj_comm {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) (w : V) : G'.Adj v w ↔ G'.Adj w v

theorem SimpleGraph.Subgraph.adj_symm {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) {u : V} {v : V} (h : G'.Adj u v) : G'.Adj v u

theorem SimpleGraph.Subgraph.Adj.symm {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {u : V} {v : V} (h : G'.Adj u v) : G'.Adj v u

theorem SimpleGraph.Subgraph.Adj.adj_sub {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {u : V} {v : V} (h : H.Adj u v) : G.Adj u v

theorem SimpleGraph.Subgraph.Adj.fst_mem {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {u : V} {v : V} (h : H.Adj u v) : u ∈ H.verts

theorem SimpleGraph.Subgraph.Adj.snd_mem {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {u : V} {v : V} (h : H.Adj u v) : v ∈ H.verts

theorem SimpleGraph.Subgraph.Adj.ne {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {u : V} {v : V} (h : H.Adj u v) : u ≠ v

@[simp]

theorem SimpleGraph.Subgraph.coe_adj {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : ↑G'.verts) (w : ↑G'.verts) : (SimpleGraph.Subgraph.coe G').Adj v w = G'.Adj ↑v ↑w

def SimpleGraph.Subgraph.coe {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) : SimpleGraph ↑G'.verts

Coercion from G' : Subgraph G to a SimpleGraph G'.verts.

Equations

• SimpleGraph.Subgraph.coe G' = { Adj := fun (v w : ↑G'.verts) => G'.Adj ↑v ↑w, symm := ⋯, loopless := ⋯ }

@[simp]

theorem SimpleGraph.Subgraph.coe_adj_sub {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (u : ↑G'.verts) (v : ↑G'.verts) (h : (SimpleGraph.Subgraph.coe G').Adj u v) : G.Adj ↑u ↑v

theorem SimpleGraph.Subgraph.Adj.coe {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {u : V} {v : V} (h : H.Adj u v) : (SimpleGraph.Subgraph.coe H).Adj { val := u, property := ⋯ } { val := v, property := ⋯ }

def SimpleGraph.Subgraph.IsSpanning {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) : Prop

A subgraph is called a spanning subgraph if it contains all the vertices of G.

Equations

• SimpleGraph.Subgraph.IsSpanning G' = ∀ (v : V), v ∈ G'.verts

theorem SimpleGraph.Subgraph.isSpanning_iff {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.IsSpanning G' ↔ G'.verts = Set.univ

@[simp]

theorem SimpleGraph.Subgraph.spanningCoe_adj {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) : ∀ (a a_1 : V), (SimpleGraph.Subgraph.spanningCoe G').Adj a a_1 = G'.Adj a a_1

def SimpleGraph.Subgraph.spanningCoe {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) : SimpleGraph V

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.

Equations

• SimpleGraph.Subgraph.spanningCoe G' = { Adj := G'.Adj, symm := ⋯, loopless := ⋯ }

@[simp]

theorem SimpleGraph.Subgraph.Adj.of_spanningCoe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {u : ↑G'.verts} {v : ↑G'.verts} (h : (SimpleGraph.Subgraph.spanningCoe G').Adj ↑u ↑v) : G.Adj ↑u ↑v

theorem SimpleGraph.Subgraph.spanningCoe_inj {V : Type u} {G : SimpleGraph V} {G₁ : SimpleGraph.Subgraph G} {G₂ : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.spanningCoe G₁ = SimpleGraph.Subgraph.spanningCoe G₂ ↔ G₁.Adj = G₂.Adj

@[simp]

theorem SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_apply_coe {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (h : SimpleGraph.Subgraph.IsSpanning G') (v : V) : ↑((SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning G' h) v) = v

@[simp]

theorem SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_symm_apply {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (h : SimpleGraph.Subgraph.IsSpanning G') (v : ↑G'.verts) : (RelIso.symm (SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning G' h)) v = ↑v

def SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (h : SimpleGraph.Subgraph.IsSpanning G') : SimpleGraph.Subgraph.spanningCoe G' ≃g SimpleGraph.Subgraph.coe G'

spanningCoe is equivalent to coe for a subgraph that IsSpanning.

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.Subgraph.IsInduced {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) : Prop

A subgraph is called an induced subgraph if vertices of G' are adjacent if they are adjacent in G.

Equations

• SimpleGraph.Subgraph.IsInduced G' = ∀ {v w : V}, v ∈ G'.verts → w ∈ G'.verts → G.Adj v w → G'.Adj v w

def SimpleGraph.Subgraph.support {V : Type u} {G : SimpleGraph V} (H : SimpleGraph.Subgraph G) : Set V

H.support is the set of vertices that form edges in the subgraph H.

Equations

• SimpleGraph.Subgraph.support H = Rel.dom H.Adj

theorem SimpleGraph.Subgraph.mem_support {V : Type u} {G : SimpleGraph V} (H : SimpleGraph.Subgraph G) {v : V} : v ∈ SimpleGraph.Subgraph.support H ↔ ∃ (w : V), H.Adj v w

theorem SimpleGraph.Subgraph.support_subset_verts {V : Type u} {G : SimpleGraph V} (H : SimpleGraph.Subgraph G) : SimpleGraph.Subgraph.support H ⊆ H.verts

def SimpleGraph.Subgraph.neighborSet {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) : Set V

G'.neighborSet v is the set of vertices adjacent to v in G'.

Equations

• SimpleGraph.Subgraph.neighborSet G' v = {w : V | G'.Adj v w}

theorem SimpleGraph.Subgraph.neighborSet_subset {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) : SimpleGraph.Subgraph.neighborSet G' v ⊆ SimpleGraph.neighborSet G v

theorem SimpleGraph.Subgraph.neighborSet_subset_verts {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) : SimpleGraph.Subgraph.neighborSet G' v ⊆ G'.verts

@[simp]

theorem SimpleGraph.Subgraph.mem_neighborSet {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) (w : V) : w ∈ SimpleGraph.Subgraph.neighborSet G' v ↔ G'.Adj v w

def SimpleGraph.Subgraph.coeNeighborSetEquiv {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (v : ↑G'.verts) : ↑(SimpleGraph.neighborSet (SimpleGraph.Subgraph.coe G') v) ≃ ↑(SimpleGraph.Subgraph.neighborSet G' ↑v)

A subgraph as a graph has equivalent neighbor sets.

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.Subgraph.edgeSet {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) : Set (Sym2 V)

The edge set of G' consists of a subset of edges of G.

Equations

• SimpleGraph.Subgraph.edgeSet G' = Sym2.fromRel ⋯

theorem SimpleGraph.Subgraph.edgeSet_subset {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) : SimpleGraph.Subgraph.edgeSet G' ⊆ SimpleGraph.edgeSet G

@[simp]

theorem SimpleGraph.Subgraph.mem_edgeSet {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {v : V} {w : V} : s(v, w) ∈ SimpleGraph.Subgraph.edgeSet G' ↔ G'.Adj v w

theorem SimpleGraph.Subgraph.mem_verts_if_mem_edge {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {e : Sym2 V} {v : V} (he : e ∈ SimpleGraph.Subgraph.edgeSet G') (hv : v ∈ e) : v ∈ G'.verts

def SimpleGraph.Subgraph.incidenceSet {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) : Set (Sym2 V)

The incidenceSet is the set of edges incident to a given vertex.

Equations

• SimpleGraph.Subgraph.incidenceSet G' v = {e : Sym2 V | e ∈ SimpleGraph.Subgraph.edgeSet G' ∧ v ∈ e}

theorem SimpleGraph.Subgraph.incidenceSet_subset_incidenceSet {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) : SimpleGraph.Subgraph.incidenceSet G' v ⊆ SimpleGraph.incidenceSet G v

theorem SimpleGraph.Subgraph.incidenceSet_subset {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) : SimpleGraph.Subgraph.incidenceSet G' v ⊆ SimpleGraph.Subgraph.edgeSet G'

@[reducible]

def SimpleGraph.Subgraph.vert {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) (h : v ∈ G'.verts) : ↑G'.verts

Give a vertex as an element of the subgraph's vertex type.

Equations

• SimpleGraph.Subgraph.vert G' v h = { val := v, property := h }

def SimpleGraph.Subgraph.copy {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (V'' : Set V) (hV : V'' = G'.verts) (adj' : V → V → Prop) (hadj : adj' = G'.Adj) : SimpleGraph.Subgraph G

Create an equal copy of a subgraph (see copy_eq) with possibly different definitional equalities. See Note [range copy pattern].

Equations

• SimpleGraph.Subgraph.copy G' V'' hV adj' hadj = { verts := V'', Adj := adj', adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

theorem SimpleGraph.Subgraph.copy_eq {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (V'' : Set V) (hV : V'' = G'.verts) (adj' : V → V → Prop) (hadj : adj' = G'.Adj) : SimpleGraph.Subgraph.copy G' V'' hV adj' hadj = G'

instance SimpleGraph.Subgraph.instSupSubgraph {V : Type u} {G : SimpleGraph V} : Sup (SimpleGraph.Subgraph G)

The union of two subgraphs.

Equations

• One or more equations did not get rendered due to their size.

instance SimpleGraph.Subgraph.instInfSubgraph {V : Type u} {G : SimpleGraph V} : Inf (SimpleGraph.Subgraph G)

The intersection of two subgraphs.

Equations

• One or more equations did not get rendered due to their size.

instance SimpleGraph.Subgraph.instTopSubgraph {V : Type u} {G : SimpleGraph V} : Top (SimpleGraph.Subgraph G)

The top subgraph is G as a subgraph of itself.

Equations

• SimpleGraph.Subgraph.instTopSubgraph = { top := { verts := Set.univ, Adj := G.Adj, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } }

instance SimpleGraph.Subgraph.instBotSubgraph {V : Type u} {G : SimpleGraph V} : Bot (SimpleGraph.Subgraph G)

The bot subgraph is the subgraph with no vertices or edges.

Equations

• SimpleGraph.Subgraph.instBotSubgraph = { bot := { verts := ∅, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } }

instance SimpleGraph.Subgraph.instSupSetSubgraph {V : Type u} {G : SimpleGraph V} : SupSet (SimpleGraph.Subgraph G)

Equations

• One or more equations did not get rendered due to their size.

instance SimpleGraph.Subgraph.instInfSetSubgraph {V : Type u} {G : SimpleGraph V} : InfSet (SimpleGraph.Subgraph G)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SimpleGraph.Subgraph.sup_adj {V : Type u} {G : SimpleGraph V} {G₁ : SimpleGraph.Subgraph G} {G₂ : SimpleGraph.Subgraph G} {a : V} {b : V} : (G₁ ⊔ G₂).Adj a b ↔ G₁.Adj a b ∨ G₂.Adj a b

@[simp]

theorem SimpleGraph.Subgraph.inf_adj {V : Type u} {G : SimpleGraph V} {G₁ : SimpleGraph.Subgraph G} {G₂ : SimpleGraph.Subgraph G} {a : V} {b : V} : (G₁ ⊓ G₂).Adj a b ↔ G₁.Adj a b ∧ G₂.Adj a b

@[simp]

theorem SimpleGraph.Subgraph.top_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} : ⊤.Adj a b ↔ G.Adj a b

@[simp]

theorem SimpleGraph.Subgraph.not_bot_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} : ¬⊥.Adj a b

@[simp]

theorem SimpleGraph.Subgraph.verts_sup {V : Type u} {G : SimpleGraph V} (G₁ : SimpleGraph.Subgraph G) (G₂ : SimpleGraph.Subgraph G) : (G₁ ⊔ G₂).verts = G₁.verts ∪ G₂.verts

@[simp]

theorem SimpleGraph.Subgraph.verts_inf {V : Type u} {G : SimpleGraph V} (G₁ : SimpleGraph.Subgraph G) (G₂ : SimpleGraph.Subgraph G) : (G₁ ⊓ G₂).verts = G₁.verts ∩ G₂.verts

@[simp]

theorem SimpleGraph.Subgraph.verts_top {V : Type u} {G : SimpleGraph V} : ⊤.verts = Set.univ

@[simp]

theorem SimpleGraph.Subgraph.verts_bot {V : Type u} {G : SimpleGraph V} : ⊥.verts = ∅

@[simp]

theorem SimpleGraph.Subgraph.sSup_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {s : Set (SimpleGraph.Subgraph G)} : (sSup s).Adj a b ↔ ∃ G_1 ∈ s, G_1.Adj a b

@[simp]

theorem SimpleGraph.Subgraph.sInf_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {s : Set (SimpleGraph.Subgraph G)} : (sInf s).Adj a b ↔ (∀ G' ∈ s, G'.Adj a b) ∧ G.Adj a b

@[simp]

theorem SimpleGraph.Subgraph.iSup_adj {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {f : ι → SimpleGraph.Subgraph G} : (⨆ (i : ι), f i).Adj a b ↔ ∃ (i : ι), (f i).Adj a b

@[simp]

theorem SimpleGraph.Subgraph.iInf_adj {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {f : ι → SimpleGraph.Subgraph G} : (⨅ (i : ι), f i).Adj a b ↔ (∀ (i : ι), (f i).Adj a b) ∧ G.Adj a b

theorem SimpleGraph.Subgraph.sInf_adj_of_nonempty {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {s : Set (SimpleGraph.Subgraph G)} (hs : Set.Nonempty s) : (sInf s).Adj a b ↔ ∀ G' ∈ s, G'.Adj a b

theorem SimpleGraph.Subgraph.iInf_adj_of_nonempty {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} [Nonempty ι] {f : ι → SimpleGraph.Subgraph G} : (⨅ (i : ι), f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b

@[simp]

theorem SimpleGraph.Subgraph.verts_sSup {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) : (sSup s).verts = ⋃ G' ∈ s, G'.verts

@[simp]

theorem SimpleGraph.Subgraph.verts_sInf {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) : (sInf s).verts = ⋂ G' ∈ s, G'.verts

@[simp]

theorem SimpleGraph.Subgraph.verts_iSup {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {f : ι → SimpleGraph.Subgraph G} : (⨆ (i : ι), f i).verts = ⋃ (i : ι), (f i).verts

@[simp]

theorem SimpleGraph.Subgraph.verts_iInf {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {f : ι → SimpleGraph.Subgraph G} : (⨅ (i : ι), f i).verts = ⋂ (i : ι), (f i).verts

theorem SimpleGraph.Subgraph.verts_spanningCoe_injective {V : Type u} {G : SimpleGraph V} : Function.Injective fun (G' : SimpleGraph.Subgraph G) => (G'.verts, SimpleGraph.Subgraph.spanningCoe G')

instance SimpleGraph.Subgraph.distribLattice {V : Type u} {G : SimpleGraph V} : DistribLattice (SimpleGraph.Subgraph G)

For subgraphs G₁, G₂, G₁ ≤ G₂ iff G₁.verts ⊆ G₂.verts and ∀ a b, G₁.adj a b → G₂.adj a b.

Equations

• One or more equations did not get rendered due to their size.

instance SimpleGraph.Subgraph.instBoundedOrderSubgraphToLEToPreorderToPartialOrderToSemilatticeInfToLatticeDistribLattice {V : Type u} {G : SimpleGraph V} : BoundedOrder (SimpleGraph.Subgraph G)

Equations

• SimpleGraph.Subgraph.instBoundedOrderSubgraphToLEToPreorderToPartialOrderToSemilatticeInfToLatticeDistribLattice = BoundedOrder.mk

instance SimpleGraph.Subgraph.instCompletelyDistribLatticeSubgraph {V : Type u} {G : SimpleGraph V} : CompletelyDistribLattice (SimpleGraph.Subgraph G)

Equations

• SimpleGraph.Subgraph.instCompletelyDistribLatticeSubgraph = let __src := SimpleGraph.Subgraph.distribLattice; CompletelyDistribLattice.mk ⋯

@[simp]

theorem SimpleGraph.Subgraph.subgraphInhabited_default {V : Type u} {G : SimpleGraph V} : default = ⊥

instance SimpleGraph.Subgraph.subgraphInhabited {V : Type u} {G : SimpleGraph V} : Inhabited (SimpleGraph.Subgraph G)

Equations

• SimpleGraph.Subgraph.subgraphInhabited = { default := ⊥ }

@[simp]

theorem SimpleGraph.Subgraph.neighborSet_sup {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {H' : SimpleGraph.Subgraph G} (v : V) : SimpleGraph.Subgraph.neighborSet (H ⊔ H') v = SimpleGraph.Subgraph.neighborSet H v ∪ SimpleGraph.Subgraph.neighborSet H' v

@[simp]

theorem SimpleGraph.Subgraph.neighborSet_inf {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {H' : SimpleGraph.Subgraph G} (v : V) : SimpleGraph.Subgraph.neighborSet (H ⊓ H') v = SimpleGraph.Subgraph.neighborSet H v ∩ SimpleGraph.Subgraph.neighborSet H' v

@[simp]

theorem SimpleGraph.Subgraph.neighborSet_top {V : Type u} {G : SimpleGraph V} (v : V) : SimpleGraph.Subgraph.neighborSet ⊤ v = SimpleGraph.neighborSet G v

@[simp]

theorem SimpleGraph.Subgraph.neighborSet_bot {V : Type u} {G : SimpleGraph V} (v : V) : SimpleGraph.Subgraph.neighborSet ⊥ v = ∅

@[simp]

theorem SimpleGraph.Subgraph.neighborSet_sSup {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) (v : V) : SimpleGraph.Subgraph.neighborSet (sSup s) v = ⋃ G' ∈ s, SimpleGraph.Subgraph.neighborSet G' v

@[simp]

theorem SimpleGraph.Subgraph.neighborSet_sInf {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) (v : V) : SimpleGraph.Subgraph.neighborSet (sInf s) v = (⋂ G' ∈ s, SimpleGraph.Subgraph.neighborSet G' v) ∩ SimpleGraph.neighborSet G v

@[simp]

theorem SimpleGraph.Subgraph.neighborSet_iSup {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ι → SimpleGraph.Subgraph G) (v : V) : SimpleGraph.Subgraph.neighborSet (⨆ (i : ι), f i) v = ⋃ (i : ι), SimpleGraph.Subgraph.neighborSet (f i) v

@[simp]

theorem SimpleGraph.Subgraph.neighborSet_iInf {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ι → SimpleGraph.Subgraph G) (v : V) : SimpleGraph.Subgraph.neighborSet (⨅ (i : ι), f i) v = (⋂ (i : ι), SimpleGraph.Subgraph.neighborSet (f i) v) ∩ SimpleGraph.neighborSet G v

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_top {V : Type u} {G : SimpleGraph V} : SimpleGraph.Subgraph.edgeSet ⊤ = SimpleGraph.edgeSet G

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_bot {V : Type u} {G : SimpleGraph V} : SimpleGraph.Subgraph.edgeSet ⊥ = ∅

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_inf {V : Type u} {G : SimpleGraph V} {H₁ : SimpleGraph.Subgraph G} {H₂ : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.edgeSet (H₁ ⊓ H₂) = SimpleGraph.Subgraph.edgeSet H₁ ∩ SimpleGraph.Subgraph.edgeSet H₂

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_sup {V : Type u} {G : SimpleGraph V} {H₁ : SimpleGraph.Subgraph G} {H₂ : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.edgeSet (H₁ ⊔ H₂) = SimpleGraph.Subgraph.edgeSet H₁ ∪ SimpleGraph.Subgraph.edgeSet H₂

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_sSup {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) : SimpleGraph.Subgraph.edgeSet (sSup s) = ⋃ G' ∈ s, SimpleGraph.Subgraph.edgeSet G'

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_sInf {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) : SimpleGraph.Subgraph.edgeSet (sInf s) = (⋂ G' ∈ s, SimpleGraph.Subgraph.edgeSet G') ∩ SimpleGraph.edgeSet G

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_iSup {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ι → SimpleGraph.Subgraph G) : SimpleGraph.Subgraph.edgeSet (⨆ (i : ι), f i) = ⋃ (i : ι), SimpleGraph.Subgraph.edgeSet (f i)

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_iInf {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ι → SimpleGraph.Subgraph G) : SimpleGraph.Subgraph.edgeSet (⨅ (i : ι), f i) = (⋂ (i : ι), SimpleGraph.Subgraph.edgeSet (f i)) ∩ SimpleGraph.edgeSet G

@[simp]

theorem SimpleGraph.Subgraph.spanningCoe_top {V : Type u} {G : SimpleGraph V} : SimpleGraph.Subgraph.spanningCoe ⊤ = G

@[simp]

theorem SimpleGraph.Subgraph.spanningCoe_bot {V : Type u} {G : SimpleGraph V} : SimpleGraph.Subgraph.spanningCoe ⊥ = ⊥

@[simp]

theorem SimpleGraph.toSubgraph_verts {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H ≤ G) : (SimpleGraph.toSubgraph H h).verts = Set.univ

@[simp]

theorem SimpleGraph.toSubgraph_adj {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H ≤ G) : ∀ (a a_1 : V), (SimpleGraph.toSubgraph H h).Adj a a_1 = H.Adj a a_1

def SimpleGraph.toSubgraph {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H ≤ G) : SimpleGraph.Subgraph G

Turn a subgraph of a SimpleGraph into a member of its subgraph type.

Equations

• SimpleGraph.toSubgraph H h = { verts := Set.univ, Adj := H.Adj, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

theorem SimpleGraph.Subgraph.support_mono {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {H' : SimpleGraph.Subgraph G} (h : H ≤ H') : SimpleGraph.Subgraph.support H ⊆ SimpleGraph.Subgraph.support H'

theorem SimpleGraph.toSubgraph.isSpanning {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H ≤ G) : SimpleGraph.Subgraph.IsSpanning (SimpleGraph.toSubgraph H h)

theorem SimpleGraph.Subgraph.spanningCoe_le_of_le {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {H' : SimpleGraph.Subgraph G} (h : H ≤ H') : SimpleGraph.Subgraph.spanningCoe H ≤ SimpleGraph.Subgraph.spanningCoe H'

def SimpleGraph.Subgraph.topEquiv {V : Type u} {G : SimpleGraph V} : SimpleGraph.Subgraph.coe ⊤ ≃g G

The top of the Subgraph G lattice is equivalent to the graph itself.

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.Subgraph.botEquiv {V : Type u} {G : SimpleGraph V} : SimpleGraph.Subgraph.coe ⊥ ≃g ⊥

The bottom of the Subgraph G lattice is equivalent to the empty graph on the empty vertex type.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.Subgraph.edgeSet_mono {V : Type u} {G : SimpleGraph V} {H₁ : SimpleGraph.Subgraph G} {H₂ : SimpleGraph.Subgraph G} (h : H₁ ≤ H₂) : SimpleGraph.Subgraph.edgeSet H₁ ≤ SimpleGraph.Subgraph.edgeSet H₂

theorem Disjoint.edgeSet {V : Type u} {G : SimpleGraph V} {H₁ : SimpleGraph.Subgraph G} {H₂ : SimpleGraph.Subgraph G} (h : Disjoint H₁ H₂) : Disjoint (SimpleGraph.Subgraph.edgeSet H₁) (SimpleGraph.Subgraph.edgeSet H₂)

@[simp]

theorem SimpleGraph.Subgraph.map_verts {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G) : (SimpleGraph.Subgraph.map f H).verts = ⇑f '' H.verts

@[simp]

theorem SimpleGraph.Subgraph.map_adj {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G) : ∀ (a a_1 : W), (SimpleGraph.Subgraph.map f H).Adj a a_1 = Relation.Map H.Adj (⇑f) (⇑f) a a_1

def SimpleGraph.Subgraph.map {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G) : SimpleGraph.Subgraph G'

Graph homomorphisms induce a covariant function on subgraphs.

Equations

• SimpleGraph.Subgraph.map f H = { verts := ⇑f '' H.verts, Adj := Relation.Map H.Adj ⇑f ⇑f, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

theorem SimpleGraph.Subgraph.map_monotone {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') : Monotone (SimpleGraph.Subgraph.map f)

theorem SimpleGraph.Subgraph.map_sup {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {H : SimpleGraph.Subgraph G} {H' : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.map f (H ⊔ H') = SimpleGraph.Subgraph.map f H ⊔ SimpleGraph.Subgraph.map f H'

@[simp]

theorem SimpleGraph.Subgraph.comap_verts {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G') : (SimpleGraph.Subgraph.comap f H).verts = ⇑f ⁻¹' H.verts

@[simp]

theorem SimpleGraph.Subgraph.comap_adj {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G') (u : V) (v : V) : (SimpleGraph.Subgraph.comap f H).Adj u v = (G.Adj u v ∧ H.Adj (f u) (f v))

def SimpleGraph.Subgraph.comap {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G') : SimpleGraph.Subgraph G

Graph homomorphisms induce a contravariant function on subgraphs.

Equations

• SimpleGraph.Subgraph.comap f H = { verts := ⇑f ⁻¹' H.verts, Adj := fun (u v : V) => G.Adj u v ∧ H.Adj (f u) (f v), adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

theorem SimpleGraph.Subgraph.comap_monotone {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') : Monotone (SimpleGraph.Subgraph.comap f)

theorem SimpleGraph.Subgraph.map_le_iff_le_comap {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G) (H' : SimpleGraph.Subgraph G') : SimpleGraph.Subgraph.map f H ≤ H' ↔ H ≤ SimpleGraph.Subgraph.comap f H'

@[simp]

theorem SimpleGraph.Subgraph.inclusion_apply_coe {V : Type u} {G : SimpleGraph V} {x : SimpleGraph.Subgraph G} {y : SimpleGraph.Subgraph G} (h : x ≤ y) (v : ↑x.verts) : ↑((SimpleGraph.Subgraph.inclusion h) v) = ↑v

def SimpleGraph.Subgraph.inclusion {V : Type u} {G : SimpleGraph V} {x : SimpleGraph.Subgraph G} {y : SimpleGraph.Subgraph G} (h : x ≤ y) : SimpleGraph.Subgraph.coe x →g SimpleGraph.Subgraph.coe y

Given two subgraphs, one a subgraph of the other, there is an induced injective homomorphism of the subgraphs as graphs.

Equations

• SimpleGraph.Subgraph.inclusion h = { toFun := fun (v : ↑x.verts) => { val := ↑v, property := ⋯ }, map_rel' := ⋯ }

theorem SimpleGraph.Subgraph.inclusion.injective {V : Type u} {G : SimpleGraph V} {x : SimpleGraph.Subgraph G} {y : SimpleGraph.Subgraph G} (h : x ≤ y) : Function.Injective ⇑(SimpleGraph.Subgraph.inclusion h)

@[simp]

theorem SimpleGraph.Subgraph.hom_apply {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) (v : ↑x.verts) : (SimpleGraph.Subgraph.hom x) v = ↑v

def SimpleGraph.Subgraph.hom {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) : SimpleGraph.Subgraph.coe x →g G

There is an induced injective homomorphism of a subgraph of G into G.

Equations

• SimpleGraph.Subgraph.hom x = { toFun := fun (v : ↑x.verts) => ↑v, map_rel' := ⋯ }

@[simp]

theorem SimpleGraph.Subgraph.coe_hom {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) : ⇑(SimpleGraph.Subgraph.hom x) = fun (v : ↑x.verts) => ↑v

theorem SimpleGraph.Subgraph.hom.injective {V : Type u} {G : SimpleGraph V} {x : SimpleGraph.Subgraph G} : Function.Injective ⇑(SimpleGraph.Subgraph.hom x)

@[simp]

theorem SimpleGraph.Subgraph.spanningHom_apply {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) (a : V) : (SimpleGraph.Subgraph.spanningHom x) a = id a

def SimpleGraph.Subgraph.spanningHom {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) : SimpleGraph.Subgraph.spanningCoe x →g G

There is an induced injective homomorphism of a subgraph of G as a spanning subgraph into G.

Equations

• SimpleGraph.Subgraph.spanningHom x = { toFun := id, map_rel' := ⋯ }

theorem SimpleGraph.Subgraph.spanningHom.injective {V : Type u} {G : SimpleGraph V} {x : SimpleGraph.Subgraph G} : Function.Injective ⇑(SimpleGraph.Subgraph.spanningHom x)

theorem SimpleGraph.Subgraph.neighborSet_subset_of_subgraph {V : Type u} {G : SimpleGraph V} {x : SimpleGraph.Subgraph G} {y : SimpleGraph.Subgraph G} (h : x ≤ y) (v : V) : SimpleGraph.Subgraph.neighborSet x v ⊆ SimpleGraph.Subgraph.neighborSet y v

instance SimpleGraph.Subgraph.neighborSet.decidablePred {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) [h : DecidableRel G'.Adj] (v : V) : DecidablePred fun (x : V) => x ∈ SimpleGraph.Subgraph.neighborSet G' v

Equations

• SimpleGraph.Subgraph.neighborSet.decidablePred G' v = h v

instance SimpleGraph.Subgraph.finiteAt {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (v : ↑G'.verts) [DecidableRel G'.Adj] [Fintype ↑(SimpleGraph.neighborSet G ↑v)] : Fintype ↑(SimpleGraph.Subgraph.neighborSet G' ↑v)

If a graph is locally finite at a vertex, then so is a subgraph of that graph.

Equations

• SimpleGraph.Subgraph.finiteAt v = Set.fintypeSubset (SimpleGraph.neighborSet G ↑v) ⋯

def SimpleGraph.Subgraph.finiteAtOfSubgraph {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {G'' : SimpleGraph.Subgraph G} [DecidableRel G'.Adj] (h : G' ≤ G'') (v : ↑G'.verts) [Fintype ↑(SimpleGraph.Subgraph.neighborSet G'' ↑v)] : Fintype ↑(SimpleGraph.Subgraph.neighborSet G' ↑v)

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.

Equations

• SimpleGraph.Subgraph.finiteAtOfSubgraph h v = Set.fintypeSubset (SimpleGraph.Subgraph.neighborSet G'' ↑v) ⋯

instance SimpleGraph.Subgraph.instFintypeElemNeighborSet {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) [Fintype ↑G'.verts] (v : V) [DecidablePred fun (x : V) => x ∈ SimpleGraph.Subgraph.neighborSet G' v] : Fintype ↑(SimpleGraph.Subgraph.neighborSet G' v)

Equations

• SimpleGraph.Subgraph.instFintypeElemNeighborSet G' v = Set.fintypeSubset G'.verts ⋯

instance SimpleGraph.Subgraph.coeFiniteAt {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (v : ↑G'.verts) [Fintype ↑(SimpleGraph.Subgraph.neighborSet G' ↑v)] : Fintype ↑(SimpleGraph.neighborSet (SimpleGraph.Subgraph.coe G') v)

Equations

• SimpleGraph.Subgraph.coeFiniteAt v = Fintype.ofEquiv (↑(SimpleGraph.Subgraph.neighborSet G' ↑v)) (SimpleGraph.Subgraph.coeNeighborSetEquiv v).symm

theorem SimpleGraph.Subgraph.IsSpanning.card_verts {V : Type u} {G : SimpleGraph V} [Fintype V] {G' : SimpleGraph.Subgraph G} [Fintype ↑G'.verts] (h : SimpleGraph.Subgraph.IsSpanning G') : (Set.toFinset G'.verts).card = Fintype.card V

def SimpleGraph.Subgraph.degree {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) [Fintype ↑(SimpleGraph.Subgraph.neighborSet G' v)] : ℕ

The degree of a vertex in a subgraph. It's zero for vertices outside the subgraph.

Equations

• SimpleGraph.Subgraph.degree G' v = Fintype.card ↑(SimpleGraph.Subgraph.neighborSet G' v)

theorem SimpleGraph.Subgraph.finset_card_neighborSet_eq_degree {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {v : V} [Fintype ↑(SimpleGraph.Subgraph.neighborSet G' v)] : (Set.toFinset (SimpleGraph.Subgraph.neighborSet G' v)).card = SimpleGraph.Subgraph.degree G' v

theorem SimpleGraph.Subgraph.degree_le {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) [Fintype ↑(SimpleGraph.Subgraph.neighborSet G' v)] [Fintype ↑(SimpleGraph.neighborSet G v)] : SimpleGraph.Subgraph.degree G' v ≤ SimpleGraph.degree G v

theorem SimpleGraph.Subgraph.degree_le' {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (G'' : SimpleGraph.Subgraph G) (h : G' ≤ G'') (v : V) [Fintype ↑(SimpleGraph.Subgraph.neighborSet G' v)] [Fintype ↑(SimpleGraph.Subgraph.neighborSet G'' v)] : SimpleGraph.Subgraph.degree G' v ≤ SimpleGraph.Subgraph.degree G'' v

@[simp]

theorem SimpleGraph.Subgraph.coe_degree {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : ↑G'.verts) [Fintype ↑(SimpleGraph.neighborSet (SimpleGraph.Subgraph.coe G') v)] [Fintype ↑(SimpleGraph.Subgraph.neighborSet G' ↑v)] : SimpleGraph.degree (SimpleGraph.Subgraph.coe G') v = SimpleGraph.Subgraph.degree G' ↑v

@[simp]

theorem SimpleGraph.Subgraph.degree_spanningCoe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (v : V) [Fintype ↑(SimpleGraph.Subgraph.neighborSet G' v)] [Fintype ↑(SimpleGraph.neighborSet (SimpleGraph.Subgraph.spanningCoe G') v)] : SimpleGraph.degree (SimpleGraph.Subgraph.spanningCoe G') v = SimpleGraph.Subgraph.degree G' v

theorem SimpleGraph.Subgraph.degree_eq_one_iff_unique_adj {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {v : V} [Fintype ↑(SimpleGraph.Subgraph.neighborSet G' v)] : SimpleGraph.Subgraph.degree G' v = 1 ↔ ∃! (w : V), G'.Adj v w

Properties of singletonSubgraph and subgraphOfAdj

instance SimpleGraph.nonempty_singletonSubgraph_verts {V : Type u} {G : SimpleGraph V} (v : V) : Nonempty ↑(SimpleGraph.singletonSubgraph G v).verts

Equations

• ⋯ = ⋯

@[simp]

theorem SimpleGraph.singletonSubgraph_le_iff {V : Type u} {G : SimpleGraph V} (v : V) (H : SimpleGraph.Subgraph G) : SimpleGraph.singletonSubgraph G v ≤ H ↔ v ∈ H.verts

@[simp]

theorem SimpleGraph.map_singletonSubgraph {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V} : SimpleGraph.Subgraph.map f (SimpleGraph.singletonSubgraph G v) = SimpleGraph.singletonSubgraph G' (f v)

@[simp]

theorem SimpleGraph.neighborSet_singletonSubgraph {V : Type u} {G : SimpleGraph V} (v : V) (w : V) : SimpleGraph.Subgraph.neighborSet (SimpleGraph.singletonSubgraph G v) w = ∅

@[simp]

theorem SimpleGraph.edgeSet_singletonSubgraph {V : Type u} {G : SimpleGraph V} (v : V) : SimpleGraph.Subgraph.edgeSet (SimpleGraph.singletonSubgraph G v) = ∅

theorem SimpleGraph.eq_singletonSubgraph_iff_verts_eq {V : Type u} {G : SimpleGraph V} (H : SimpleGraph.Subgraph G) {v : V} : H = SimpleGraph.singletonSubgraph G v ↔ H.verts = {v}

instance SimpleGraph.nonempty_subgraphOfAdj_verts {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) : Nonempty ↑(SimpleGraph.subgraphOfAdj G hvw).verts

Equations

• ⋯ = ⋯

@[simp]

theorem SimpleGraph.edgeSet_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) : SimpleGraph.Subgraph.edgeSet (SimpleGraph.subgraphOfAdj G hvw) = {s(v, w)}

theorem SimpleGraph.subgraphOfAdj_le_of_adj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (H : SimpleGraph.Subgraph G) (h : H.Adj v w) : SimpleGraph.subgraphOfAdj G ⋯ ≤ H

theorem SimpleGraph.subgraphOfAdj_symm {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) : SimpleGraph.subgraphOfAdj G ⋯ = SimpleGraph.subgraphOfAdj G hvw

@[simp]

theorem SimpleGraph.map_subgraphOfAdj {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V} {w : V} (hvw : G.Adj v w) : SimpleGraph.Subgraph.map f (SimpleGraph.subgraphOfAdj G hvw) = SimpleGraph.subgraphOfAdj G' ⋯

theorem SimpleGraph.neighborSet_subgraphOfAdj_subset {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (hvw : G.Adj v w) : SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) u ⊆ {v, w}

@[simp]

theorem SimpleGraph.neighborSet_fst_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) : SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) v = {w}

@[simp]

theorem SimpleGraph.neighborSet_snd_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) : SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) w = {v}

@[simp]

theorem SimpleGraph.neighborSet_subgraphOfAdj_of_ne_of_ne {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (hvw : G.Adj v w) (hv : u ≠ v) (hw : u ≠ w) : SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) u = ∅

theorem SimpleGraph.neighborSet_subgraphOfAdj {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (hvw : G.Adj v w) : SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅

theorem SimpleGraph.singletonSubgraph_fst_le_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {h : G.Adj u v} : SimpleGraph.singletonSubgraph G u ≤ SimpleGraph.subgraphOfAdj G h

theorem SimpleGraph.singletonSubgraph_snd_le_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {h : G.Adj u v} : SimpleGraph.singletonSubgraph G v ≤ SimpleGraph.subgraphOfAdj G h

Subgraphs of subgraphs

@[reducible]

def SimpleGraph.Subgraph.coeSubgraph {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph (SimpleGraph.Subgraph.coe G') → SimpleGraph.Subgraph G

Given a subgraph of a subgraph of G, construct a subgraph of G.

Equations

• SimpleGraph.Subgraph.coeSubgraph = SimpleGraph.Subgraph.map (SimpleGraph.Subgraph.hom G')

@[reducible]

def SimpleGraph.Subgraph.restrict {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph G → SimpleGraph.Subgraph (SimpleGraph.Subgraph.coe G')

Given a subgraph of G, restrict it to being a subgraph of another subgraph G' by taking the portion of G that intersects G'.

Equations

• SimpleGraph.Subgraph.restrict = SimpleGraph.Subgraph.comap (SimpleGraph.Subgraph.hom G')

theorem SimpleGraph.Subgraph.coeSubgraph_adj {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (G'' : SimpleGraph.Subgraph (SimpleGraph.Subgraph.coe G')) (v : V) (w : V) : (SimpleGraph.Subgraph.coeSubgraph G'').Adj v w ↔ ∃ (hv : v ∈ G'.verts) (hw : w ∈ G'.verts), G''.Adj { val := v, property := hv } { val := w, property := hw }

theorem SimpleGraph.Subgraph.restrict_adj {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {G'' : SimpleGraph.Subgraph G} (v : ↑G'.verts) (w : ↑G'.verts) : (SimpleGraph.Subgraph.restrict G'').Adj v w ↔ G'.Adj ↑v ↑w ∧ G''.Adj ↑v ↑w

theorem SimpleGraph.Subgraph.restrict_coeSubgraph {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (G'' : SimpleGraph.Subgraph (SimpleGraph.Subgraph.coe G')) : SimpleGraph.Subgraph.restrict (SimpleGraph.Subgraph.coeSubgraph G'') = G''

theorem SimpleGraph.Subgraph.coeSubgraph_injective {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) : Function.Injective SimpleGraph.Subgraph.coeSubgraph

theorem SimpleGraph.Subgraph.coeSubgraph_le {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} (H' : SimpleGraph.Subgraph (SimpleGraph.Subgraph.coe H)) : SimpleGraph.Subgraph.coeSubgraph H' ≤ H

theorem SimpleGraph.Subgraph.coeSubgraph_restrict_eq {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} (H' : SimpleGraph.Subgraph G) : SimpleGraph.Subgraph.coeSubgraph (SimpleGraph.Subgraph.restrict H') = H ⊓ H'

Edge deletion

def SimpleGraph.Subgraph.deleteEdges {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (s : Set (Sym2 V)) : SimpleGraph.Subgraph G

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.

Equations

• SimpleGraph.Subgraph.deleteEdges G' s = { verts := G'.verts, Adj := G'.Adj \ Sym2.ToRel s, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

@[simp]

theorem SimpleGraph.Subgraph.deleteEdges_verts {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set (Sym2 V)) : (SimpleGraph.Subgraph.deleteEdges G' s).verts = G'.verts

@[simp]

theorem SimpleGraph.Subgraph.deleteEdges_adj {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set (Sym2 V)) (v : V) (w : V) : (SimpleGraph.Subgraph.deleteEdges G' s).Adj v w ↔ G'.Adj v w ∧ s(v, w) ∉ s

@[simp]

theorem SimpleGraph.Subgraph.deleteEdges_deleteEdges {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set (Sym2 V)) (s' : Set (Sym2 V)) : SimpleGraph.Subgraph.deleteEdges (SimpleGraph.Subgraph.deleteEdges G' s) s' = SimpleGraph.Subgraph.deleteEdges G' (s ∪ s')

@[simp]

theorem SimpleGraph.Subgraph.deleteEdges_empty_eq {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.deleteEdges G' ∅ = G'

@[simp]

theorem SimpleGraph.Subgraph.deleteEdges_spanningCoe_eq {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set (Sym2 V)) : SimpleGraph.deleteEdges (SimpleGraph.Subgraph.spanningCoe G') s = SimpleGraph.Subgraph.spanningCoe (SimpleGraph.Subgraph.deleteEdges G' s)

theorem SimpleGraph.Subgraph.deleteEdges_coe_eq {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set (Sym2 ↑G'.verts)) : SimpleGraph.deleteEdges (SimpleGraph.Subgraph.coe G') s = SimpleGraph.Subgraph.coe (SimpleGraph.Subgraph.deleteEdges G' (Sym2.map Subtype.val '' s))

theorem SimpleGraph.Subgraph.coe_deleteEdges_eq {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set (Sym2 V)) : SimpleGraph.Subgraph.coe (SimpleGraph.Subgraph.deleteEdges G' s) = SimpleGraph.deleteEdges (SimpleGraph.Subgraph.coe G') (Sym2.map Subtype.val ⁻¹' s)

theorem SimpleGraph.Subgraph.deleteEdges_le {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set (Sym2 V)) : SimpleGraph.Subgraph.deleteEdges G' s ≤ G'

theorem SimpleGraph.Subgraph.deleteEdges_le_of_le {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set (Sym2 V)} {s' : Set (Sym2 V)} (h : s ⊆ s') : SimpleGraph.Subgraph.deleteEdges G' s' ≤ SimpleGraph.Subgraph.deleteEdges G' s

@[simp]

theorem SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_left_eq {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set (Sym2 V)) : SimpleGraph.Subgraph.deleteEdges G' (SimpleGraph.Subgraph.edgeSet G' ∩ s) = SimpleGraph.Subgraph.deleteEdges G' s

@[simp]

theorem SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_right_eq {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set (Sym2 V)) : SimpleGraph.Subgraph.deleteEdges G' (s ∩ SimpleGraph.Subgraph.edgeSet G') = SimpleGraph.Subgraph.deleteEdges G' s

theorem SimpleGraph.Subgraph.coe_deleteEdges_le {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set (Sym2 V)) : SimpleGraph.Subgraph.coe (SimpleGraph.Subgraph.deleteEdges G' s) ≤ SimpleGraph.Subgraph.coe G'

theorem SimpleGraph.Subgraph.spanningCoe_deleteEdges_le {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (s : Set (Sym2 V)) : SimpleGraph.Subgraph.spanningCoe (SimpleGraph.Subgraph.deleteEdges G' s) ≤ SimpleGraph.Subgraph.spanningCoe G'

Induced subgraphs

@[simp]

theorem SimpleGraph.Subgraph.induce_adj {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (s : Set V) (u : V) (v : V) : (SimpleGraph.Subgraph.induce G' s).Adj u v = (u ∈ s ∧ v ∈ s ∧ G'.Adj u v)

@[simp]

theorem SimpleGraph.Subgraph.induce_verts {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (s : Set V) : (SimpleGraph.Subgraph.induce G' s).verts = s

def SimpleGraph.Subgraph.induce {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (s : Set V) : SimpleGraph.Subgraph G

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'.

Equations

• SimpleGraph.Subgraph.induce G' s = { verts := s, Adj := fun (u v : V) => u ∈ s ∧ v ∈ s ∧ G'.Adj u v, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

theorem SimpleGraph.induce_eq_coe_induce_top {V : Type u} {G : SimpleGraph V} (s : Set V) : SimpleGraph.induce s G = SimpleGraph.Subgraph.coe (SimpleGraph.Subgraph.induce ⊤ s)

theorem SimpleGraph.Subgraph.induce_mono {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {G'' : SimpleGraph.Subgraph G} {s : Set V} {s' : Set V} (hg : G' ≤ G'') (hs : s ⊆ s') : SimpleGraph.Subgraph.induce G' s ≤ SimpleGraph.Subgraph.induce G'' s'

theorem SimpleGraph.Subgraph.induce_mono_left {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {G'' : SimpleGraph.Subgraph G} {s : Set V} (hg : G' ≤ G'') : SimpleGraph.Subgraph.induce G' s ≤ SimpleGraph.Subgraph.induce G'' s

theorem SimpleGraph.Subgraph.induce_mono_right {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set V} {s' : Set V} (hs : s ⊆ s') : SimpleGraph.Subgraph.induce G' s ≤ SimpleGraph.Subgraph.induce G' s'

@[simp]

theorem SimpleGraph.Subgraph.induce_empty {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.induce G' ∅ = ⊥

@[simp]

theorem SimpleGraph.Subgraph.induce_self_verts {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.induce G' G'.verts = G'

theorem SimpleGraph.Subgraph.le_induce_top_verts {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} : G' ≤ SimpleGraph.Subgraph.induce ⊤ G'.verts

theorem SimpleGraph.Subgraph.le_induce_union {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set V} {s' : Set V} : SimpleGraph.Subgraph.induce G' s ⊔ SimpleGraph.Subgraph.induce G' s' ≤ SimpleGraph.Subgraph.induce G' (s ∪ s')

theorem SimpleGraph.Subgraph.le_induce_union_left {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set V} {s' : Set V} : SimpleGraph.Subgraph.induce G' s ≤ SimpleGraph.Subgraph.induce G' (s ∪ s')

theorem SimpleGraph.Subgraph.le_induce_union_right {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set V} {s' : Set V} : SimpleGraph.Subgraph.induce G' s' ≤ SimpleGraph.Subgraph.induce G' (s ∪ s')

theorem SimpleGraph.Subgraph.singletonSubgraph_eq_induce {V : Type u} {G : SimpleGraph V} {v : V} : SimpleGraph.singletonSubgraph G v = SimpleGraph.Subgraph.induce ⊤ {v}

theorem SimpleGraph.Subgraph.subgraphOfAdj_eq_induce {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) : SimpleGraph.subgraphOfAdj G hvw = SimpleGraph.Subgraph.induce ⊤ {v, w}

@[reducible]

def SimpleGraph.Subgraph.deleteVerts {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (s : Set V) : SimpleGraph.Subgraph G

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.

Equations

• SimpleGraph.Subgraph.deleteVerts G' s = SimpleGraph.Subgraph.induce G' (G'.verts \ s)

theorem SimpleGraph.Subgraph.deleteVerts_verts {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set V} : (SimpleGraph.Subgraph.deleteVerts G' s).verts = G'.verts \ s

theorem SimpleGraph.Subgraph.deleteVerts_adj {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set V} {u : V} {v : V} : (SimpleGraph.Subgraph.deleteVerts G' s).Adj u v ↔ u ∈ G'.verts ∧ u ∉ s ∧ v ∈ G'.verts ∧ v ∉ s ∧ G'.Adj u v

@[simp]

theorem SimpleGraph.Subgraph.deleteVerts_deleteVerts {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (s : Set V) (s' : Set V) : SimpleGraph.Subgraph.deleteVerts (SimpleGraph.Subgraph.deleteVerts G' s) s' = SimpleGraph.Subgraph.deleteVerts G' (s ∪ s')

@[simp]

theorem SimpleGraph.Subgraph.deleteVerts_empty {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.deleteVerts G' ∅ = G'

theorem SimpleGraph.Subgraph.deleteVerts_le {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set V} : SimpleGraph.Subgraph.deleteVerts G' s ≤ G'

theorem SimpleGraph.Subgraph.deleteVerts_mono {V : Type u} {G : SimpleGraph V} {s : Set V} {G' : SimpleGraph.Subgraph G} {G'' : SimpleGraph.Subgraph G} (h : G' ≤ G'') : SimpleGraph.Subgraph.deleteVerts G' s ≤ SimpleGraph.Subgraph.deleteVerts G'' s

theorem SimpleGraph.Subgraph.deleteVerts_anti {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set V} {s' : Set V} (h : s ⊆ s') : SimpleGraph.Subgraph.deleteVerts G' s' ≤ SimpleGraph.Subgraph.deleteVerts G' s

@[simp]

theorem SimpleGraph.Subgraph.deleteVerts_inter_verts_left_eq {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set V} : SimpleGraph.Subgraph.deleteVerts G' (G'.verts ∩ s) = SimpleGraph.Subgraph.deleteVerts G' s

@[simp]

theorem SimpleGraph.Subgraph.deleteVerts_inter_verts_set_right_eq {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {s : Set V} : SimpleGraph.Subgraph.deleteVerts G' (s ∩ G'.verts) = SimpleGraph.Subgraph.deleteVerts G' s