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.

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

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

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

The one-vertex subgraph.

Equations

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

@[simp]

theorem SimpleGraph.singletonSubgraph_adj {V : Type u} (G : SimpleGraph V) (v a✝ a✝¹ : V) : (G.singletonSubgraph v).Adj a✝ a✝¹ = ⊥ a✝ a✝¹

@[simp]

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

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

The one-edge subgraph.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

instance SimpleGraph.Subgraph.instDecidableRelElemVertsAdjCoeOfAdj {V : Type u} (G : SimpleGraph V) (H : G.Subgraph) [DecidableRel H.Adj] : DecidableRel H.coe.Adj

Equations

• SimpleGraph.Subgraph.instDecidableRelElemVertsAdjCoeOfAdj G H a b = inst✝ ↑a ↑b

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

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

Equations

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

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

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

Alias of the forward direction of SimpleGraph.Subgraph.isSpanning_iff.

def SimpleGraph.Subgraph.spanningCoe {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) : 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

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

@[simp]

theorem SimpleGraph.Subgraph.spanningCoe_adj {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (a✝ a✝¹ : V) : G'.spanningCoe.Adj a✝ a✝¹ = G'.Adj a✝ a✝¹

@[simp]

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

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

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

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

spanningCoe is equivalent to coe for a subgraph that IsSpanning.

Equations

• G'.spanningCoeEquivCoeOfSpanning h = { toFun := fun (v : V) => ⟨v, ⋯⟩, invFun := fun (v : ↑G'.verts) => ↑v, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• G'.IsInduced = ∀ {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 : G.Subgraph) : Set V

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

Equations

• H.support = Rel.dom H.Adj

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

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

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

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

Equations

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

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

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

@[simp]

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

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

A subgraph as a graph has equivalent neighbor sets.

Equations

• SimpleGraph.Subgraph.coeNeighborSetEquiv v = { toFun := fun (w : ↑(G'.coe.neighborSet v)) => ⟨↑↑w, ⋯⟩, invFun := fun (w : ↑(G'.neighborSet ↑v)) => ⟨⟨↑w, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

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

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

Equations

• G'.edgeSet = Sym2.fromRel ⋯

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

@[simp]

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

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_coe {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} : G'.coe.edgeSet = Sym2.map Subtype.val ⁻¹' G'.edgeSet

theorem SimpleGraph.Subgraph.image_coe_edgeSet_coe {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) : Sym2.map Subtype.val '' G'.coe.edgeSet = G'.edgeSet

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

@[deprecated SimpleGraph.Subgraph.mem_verts_of_mem_edge]

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

Alias of SimpleGraph.Subgraph.mem_verts_of_mem_edge.

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

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

Equations

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

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

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

@[reducible, inline]

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

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

Equations

• G'.vert v h = ⟨v, h⟩

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

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

Equations

• G'.copy 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' : G.Subgraph) (V'' : Set V) (hV : V'' = G'.verts) (adj' : V → V → Prop) (hadj : adj' = G'.Adj) : G'.copy V'' hV adj' hadj = G'

instance SimpleGraph.Subgraph.instMax {V : Type u} {G : SimpleGraph V} : Max G.Subgraph

The union of two subgraphs.

Equations

• SimpleGraph.Subgraph.instMax = { max := fun (G₁ G₂ : G.Subgraph) => { verts := G₁.verts ∪ G₂.verts, Adj := G₁.Adj ⊔ G₂.Adj, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } }

instance SimpleGraph.Subgraph.instMin {V : Type u} {G : SimpleGraph V} : Min G.Subgraph

The intersection of two subgraphs.

Equations

• SimpleGraph.Subgraph.instMin = { min := fun (G₁ G₂ : G.Subgraph) => { verts := G₁.verts ∩ G₂.verts, Adj := G₁.Adj ⊓ G₂.Adj, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } }

instance SimpleGraph.Subgraph.instTop {V : Type u} {G : SimpleGraph V} : Top G.Subgraph

The top subgraph is G as a subgraph of itself.

Equations

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

instance SimpleGraph.Subgraph.instBot {V : Type u} {G : SimpleGraph V} : Bot G.Subgraph

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

Equations

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

instance SimpleGraph.Subgraph.instSupSet {V : Type u} {G : SimpleGraph V} : SupSet G.Subgraph

Equations

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

instance SimpleGraph.Subgraph.instInfSet {V : Type u} {G : SimpleGraph V} : InfSet G.Subgraph

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₁ G₂ : G.Subgraph} {a 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₁ G₂ : G.Subgraph} {a 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 b : V} : ⊤.Adj a b ↔ G.Adj a b

@[simp]

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

@[simp]

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

@[simp]

theorem SimpleGraph.Subgraph.verts_inf {V : Type u} {G : SimpleGraph V} (G₁ G₂ : G.Subgraph) : (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 b : V} {s : Set G.Subgraph} : (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 b : V} {s : Set G.Subgraph} : (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 b : V} {f : ι → G.Subgraph} : (⨆ (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 b : V} {f : ι → G.Subgraph} : (⨅ (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 b : V} {s : Set G.Subgraph} (hs : s.Nonempty) : (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 b : V} [Nonempty ι] {f : ι → G.Subgraph} : (⨅ (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 G.Subgraph) : (sSup s).verts = ⋃ G' ∈ s, G'.verts

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem SimpleGraph.Subgraph.coe_bot {V : Type u} {G : SimpleGraph V} : ⊥.coe = ⊥

@[simp]

theorem SimpleGraph.Subgraph.IsInduced.top {V : Type u} {G : SimpleGraph V} : ⊤.IsInduced

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

The graph isomorphism between the top element of G.subgraph and G.

Equations

• SimpleGraph.Subgraph.topIso = { toFun := Subtype.val, invFun := fun (a : V) => ⟨a, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

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

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

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

Equations

• SimpleGraph.Subgraph.distribLattice = DistribLattice.mk ⋯

instance SimpleGraph.Subgraph.instBoundedOrder {V : Type u} {G : SimpleGraph V} : BoundedOrder G.Subgraph

Equations

• SimpleGraph.Subgraph.instBoundedOrder = BoundedOrder.mk

def SimpleGraph.Subgraph.completelyDistribLatticeMinimalAxioms {V : Type u} {G : SimpleGraph V} : CompletelyDistribLattice.MinimalAxioms G.Subgraph

Note that subgraphs do not form a Boolean algebra, because of verts.

Equations

• SimpleGraph.Subgraph.completelyDistribLatticeMinimalAxioms = { toCompleteLattice := CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯, iInf_iSup_eq := ⋯ }

instance SimpleGraph.Subgraph.instCompletelyDistribLattice {V : Type u} {G : SimpleGraph V} : CompletelyDistribLattice G.Subgraph

Equations

• SimpleGraph.Subgraph.instCompletelyDistribLattice = CompletelyDistribLattice.ofMinimalAxioms SimpleGraph.Subgraph.completelyDistribLatticeMinimalAxioms

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

theorem SimpleGraph.Subgraph.verts_monotone {V : Type u} {G : SimpleGraph V} : Monotone SimpleGraph.Subgraph.verts

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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 := ⋯ }

@[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✝¹ : V) : (SimpleGraph.toSubgraph H h).Adj a✝ a✝¹ = H.Adj a✝ a✝¹

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

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

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

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

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

Equations

• SimpleGraph.Subgraph.topEquiv = { toFun := fun (v : ↑⊤.verts) => ↑v, invFun := fun (v : V) => ⟨v, trivial⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

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

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

Equations

• SimpleGraph.Subgraph.botEquiv = { toFun := fun (v : ↑⊥.verts) => False.elim ⋯, invFun := fun (v : Empty) => v.elim, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

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

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

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

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 := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem SimpleGraph.Subgraph.map_id {V : Type u} {G : SimpleGraph V} (H : G.Subgraph) : SimpleGraph.Subgraph.map SimpleGraph.Hom.id H = H

theorem SimpleGraph.Subgraph.map_comp {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} {U : Type u_2} {G'' : SimpleGraph U} (H : G.Subgraph) (f : G →g G') (g : G' →g G'') : SimpleGraph.Subgraph.map (g.comp f) H = SimpleGraph.Subgraph.map g (SimpleGraph.Subgraph.map f H)

theorem SimpleGraph.Subgraph.map_mono {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} {f : G →g G'} {H₁ H₂ : G.Subgraph} (hH : H₁ ≤ H₂) : SimpleGraph.Subgraph.map f H₁ ≤ SimpleGraph.Subgraph.map f H₂

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₁ H₂ : G.Subgraph) : SimpleGraph.Subgraph.map f (H₁ ⊔ H₂) = SimpleGraph.Subgraph.map f H₁ ⊔ SimpleGraph.Subgraph.map f H₂

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

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 := ⋯ }

@[simp]

theorem SimpleGraph.Subgraph.comap_verts {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G'.Subgraph) : (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 : G'.Subgraph) (u v : V) : (SimpleGraph.Subgraph.comap f H).Adj u v = (G.Adj u v ∧ H.Adj (f u) (f v))

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 : G.Subgraph) (H' : G'.Subgraph) : SimpleGraph.Subgraph.map f H ≤ H' ↔ H ≤ SimpleGraph.Subgraph.comap f H'

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

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) => ⟨↑v, ⋯⟩, map_rel' := ⋯ }

@[simp]

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Equations

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

@[simp]

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

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

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

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

Equations

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

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

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

Equations

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

def SimpleGraph.Subgraph.finiteAtOfSubgraph {V : Type u} {G : SimpleGraph V} {G' G'' : G.Subgraph} [DecidableRel G'.Adj] (h : G' ≤ G'') (v : ↑G'.verts) [Fintype ↑(G''.neighborSet ↑v)] : Fintype ↑(G'.neighborSet ↑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 = (G''.neighborSet ↑v).fintypeSubset ⋯

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

Equations

• G'.instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet v = G'.verts.fintypeSubset ⋯

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

Equations

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

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

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

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

Equations

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

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

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

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

@[simp]

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

@[simp]

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

theorem SimpleGraph.Subgraph.degree_eq_one_iff_unique_adj {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v : V} [Fintype ↑(G'.neighborSet v)] : G'.degree 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 ↑(G.singletonSubgraph v).verts

@[simp]

theorem SimpleGraph.singletonSubgraph_le_iff {V : Type u} {G : SimpleGraph V} (v : V) (H : G.Subgraph) : G.singletonSubgraph 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 (G.singletonSubgraph v) = G'.singletonSubgraph (f v)

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem SimpleGraph.neighborSet_subgraphOfAdj {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (hvw : G.Adj v w) : (G.subgraphOfAdj hvw).neighborSet 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} {h : G.Adj u v} : G.singletonSubgraph u ≤ G.subgraphOfAdj h

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

@[simp]

theorem SimpleGraph.support_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : (G.subgraphOfAdj h).support = {u, v}

Subgraphs of subgraphs

@[reducible, inline]

abbrev SimpleGraph.Subgraph.coeSubgraph {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} : G'.coe.Subgraph → G.Subgraph

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

Equations

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

@[reducible, inline]

abbrev SimpleGraph.Subgraph.restrict {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} : G.Subgraph → G'.coe.Subgraph

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

@[simp]

theorem SimpleGraph.Subgraph.verts_coeSubgraph {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (G'' : G'.coe.Subgraph) : (SimpleGraph.Subgraph.coeSubgraph G'').verts = Subtype.val '' G''.verts

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

theorem SimpleGraph.Subgraph.restrict_adj {V : Type u} {G : SimpleGraph V} {G' G'' : G.Subgraph} (v 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' : G.Subgraph} (G'' : G'.coe.Subgraph) : SimpleGraph.Subgraph.restrict (SimpleGraph.Subgraph.coeSubgraph G'') = G''

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

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

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

Edge deletion

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

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

• G'.deleteEdges 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' : G.Subgraph} (s : Set (Sym2 V)) : (G'.deleteEdges s).verts = G'.verts

@[simp]

theorem SimpleGraph.Subgraph.deleteEdges_adj {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) (v w : V) : (G'.deleteEdges 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' : G.Subgraph} (s s' : Set (Sym2 V)) : (G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s')

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

Induced subgraphs

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

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

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

@[simp]

theorem SimpleGraph.Subgraph.induce_adj {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set V) (u v : V) : (G'.induce 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' : G.Subgraph) (s : Set V) : (G'.induce s).verts = s

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[reducible, inline]

abbrev SimpleGraph.Subgraph.deleteVerts {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set V) : G.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.

Equations

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

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

theorem SimpleGraph.Subgraph.deleteVerts_adj {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} {u v : V} : (G'.deleteVerts 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' : G.Subgraph} (s s' : Set V) : (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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