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.

source

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

source

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

source

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

Type u

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

A subgraph of a SimpleGraph is a subset of vertices along with a restriction of the adjacency relation that is symmetric and is supported by the vertex subset. They also form a bounded lattice.

Thinking of V → V → Prop as Set (V × V), a set of darts (i.e., half-edges), then Subgraph.adj_sub is that the darts of a subgraph are a subset of the darts of G.

Instances For

source

@[simp]

theorem SimpleGraph.singletonSubgraph_Adj {V : Type u} (G : SimpleGraph V) (v : V) :

∀ (a a_1 : V), SimpleGraph.Subgraph.Adj (SimpleGraph.singletonSubgraph G v) a a_1 = ⊥ a a_1

source

@[simp]

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

(SimpleGraph.singletonSubgraph G v).verts = {v}

source

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

SimpleGraph.Subgraph G

The one-vertex subgraph.

Instances For

source

@[simp]

theorem SimpleGraph.subgraphOfAdj_Adj {V : Type u} (G : SimpleGraph V) {v : V} {w : V} (hvw : SimpleGraph.Adj G v w) (a : V) (b : V) :

SimpleGraph.Subgraph.Adj (SimpleGraph.subgraphOfAdj G hvw) a b = (Quotient.mk (Sym2.Rel.setoid V) (v, w) = Quotient.mk (Sym2.Rel.setoid V) (a, b))

source

@[simp]

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

(SimpleGraph.subgraphOfAdj G hvw).verts = {v, w}

source

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

SimpleGraph.Subgraph G

The one-edge subgraph.

Instances For

source

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

Irreflexive G'.Adj

source

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

SimpleGraph.Subgraph.Adj G' v w ↔ SimpleGraph.Subgraph.Adj G' w v

source

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

SimpleGraph.Subgraph.Adj G' v u

source

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

SimpleGraph.Subgraph.Adj G' v u

source

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

SimpleGraph.Adj G u v

source

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

u ∈ H.verts

source

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

v ∈ H.verts

source

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

u ≠ v

source

@[simp]

theorem SimpleGraph.Subgraph.coe_Adj {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : ↑G'.verts) (w : ↑G'.verts) :

SimpleGraph.Adj (SimpleGraph.Subgraph.coe G') v w = SimpleGraph.Subgraph.Adj G' ↑v ↑w

source

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.

Instances For

source

@[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.Adj (SimpleGraph.Subgraph.coe G') u v) :

SimpleGraph.Adj G ↑u ↑v

source

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

SimpleGraph.Adj (SimpleGraph.Subgraph.coe H) { val := u, property := (_ : u ∈ H.verts) } { val := v, property := (_ : v ∈ H.verts) }

source

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.

Instances For

source

theorem SimpleGraph.Subgraph.isSpanning_iff {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} :

SimpleGraph.Subgraph.IsSpanning G' ↔ G'.verts = Set.univ

source

@[simp]

theorem SimpleGraph.Subgraph.spanningCoe_Adj {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) :

∀ (a a_1 : V), SimpleGraph.Adj (SimpleGraph.Subgraph.spanningCoe G') a a_1 = SimpleGraph.Subgraph.Adj G' a a_1

source

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.

Instances For

source

@[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.Adj (SimpleGraph.Subgraph.spanningCoe G') ↑u ↑v) :

SimpleGraph.Adj G ↑u ↑v

source

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

source

@[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

source

@[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

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

theorem SimpleGraph.Subgraph.mem_support {V : Type u} {G : SimpleGraph V} (H : SimpleGraph.Subgraph G) {v : V} :

v ∈ SimpleGraph.Subgraph.support H ↔ ∃ w, SimpleGraph.Subgraph.Adj H v w

source

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

SimpleGraph.Subgraph.support H ⊆ H.verts

source

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

Instances For

source

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

source

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

source

@[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 ↔ SimpleGraph.Subgraph.Adj G' v w

source

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.

Instances For

source

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.

Instances For

source

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

SimpleGraph.Subgraph.edgeSet G' ⊆ SimpleGraph.edgeSet G

source

@[simp]

theorem SimpleGraph.Subgraph.mem_edgeSet {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {v : V} {w : V} :

Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ SimpleGraph.Subgraph.edgeSet G' ↔ SimpleGraph.Subgraph.Adj G' v w

source

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

source

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.

Instances For

source

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

source

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'

source

@[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.

Instances For

source

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

Instances For

source

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'

source

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

Sup (SimpleGraph.Subgraph G)

The union of two subgraphs.

source

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

Inf (SimpleGraph.Subgraph G)

The intersection of two subgraphs.

source

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

Top (SimpleGraph.Subgraph G)

The top subgraph is G as a subgraph of itself.

source

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.

source

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

SupSet (SimpleGraph.Subgraph G)

source

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

InfSet (SimpleGraph.Subgraph G)

source

@[simp]

theorem SimpleGraph.Subgraph.sup_adj {V : Type u} {G : SimpleGraph V} {G₁ : SimpleGraph.Subgraph G} {G₂ : SimpleGraph.Subgraph G} {a : V} {b : V} :

SimpleGraph.Subgraph.Adj (G₁ ⊔ G₂) a b ↔ SimpleGraph.Subgraph.Adj G₁ a b ∨ SimpleGraph.Subgraph.Adj G₂ a b

source

@[simp]

theorem SimpleGraph.Subgraph.inf_adj {V : Type u} {G : SimpleGraph V} {G₁ : SimpleGraph.Subgraph G} {G₂ : SimpleGraph.Subgraph G} {a : V} {b : V} :

SimpleGraph.Subgraph.Adj (G₁ ⊓ G₂) a b ↔ SimpleGraph.Subgraph.Adj G₁ a b ∧ SimpleGraph.Subgraph.Adj G₂ a b

source

@[simp]

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

SimpleGraph.Subgraph.Adj ⊤ a b ↔ SimpleGraph.Adj G a b

source

@[simp]

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

¬SimpleGraph.Subgraph.Adj ⊥ a b

source

@[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

source

@[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

source

@[simp]

theorem SimpleGraph.Subgraph.verts_top {V : Type u} {G : SimpleGraph V} :

⊤.verts = Set.univ

source

@[simp]

theorem SimpleGraph.Subgraph.verts_bot {V : Type u} {G : SimpleGraph V} :

⊥.verts = ∅

source

@[simp]

theorem SimpleGraph.Subgraph.sSup_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {s : Set (SimpleGraph.Subgraph G)} :

SimpleGraph.Subgraph.Adj (sSup s) a b ↔ ∃ G, G ∈ s ∧ SimpleGraph.Subgraph.Adj G a b

source

@[simp]

theorem SimpleGraph.Subgraph.sInf_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {s : Set (SimpleGraph.Subgraph G)} :

SimpleGraph.Subgraph.Adj (sInf s) a b ↔ (∀ (G' : SimpleGraph.Subgraph G), G' ∈ s → SimpleGraph.Subgraph.Adj G' a b) ∧ SimpleGraph.Adj G a b

source

@[simp]

theorem SimpleGraph.Subgraph.iSup_adj {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {f : ι → SimpleGraph.Subgraph G} :

SimpleGraph.Subgraph.Adj (⨆ (i : ι), f i) a b ↔ ∃ i, SimpleGraph.Subgraph.Adj (f i) a b

source

@[simp]

theorem SimpleGraph.Subgraph.iInf_adj {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {f : ι → SimpleGraph.Subgraph G} :

SimpleGraph.Subgraph.Adj (⨅ (i : ι), f i) a b ↔ (∀ (i : ι), SimpleGraph.Subgraph.Adj (f i) a b) ∧ SimpleGraph.Adj G a b

source

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) :

SimpleGraph.Subgraph.Adj (sInf s) a b ↔ ∀ (G' : SimpleGraph.Subgraph G), G' ∈ s → SimpleGraph.Subgraph.Adj G' a b

source

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

SimpleGraph.Subgraph.Adj (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), SimpleGraph.Subgraph.Adj (f i) a b

source

@[simp]

theorem SimpleGraph.Subgraph.verts_sSup {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) :

(sSup s).verts = ⋃ (G' : SimpleGraph.Subgraph G) (_ : G' ∈ s), G'.verts

source

@[simp]

theorem SimpleGraph.Subgraph.verts_sInf {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) :

(sInf s).verts = ⋂ (G' : SimpleGraph.Subgraph G) (_ : G' ∈ s), G'.verts

source

@[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

source

@[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

source

theorem SimpleGraph.Subgraph.verts_spanningCoe_injective {V : Type u} {G : SimpleGraph V} :

Function.Injective fun G' => (G'.verts, SimpleGraph.Subgraph.spanningCoe G')

source

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.

source

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

BoundedOrder (SimpleGraph.Subgraph G)

source

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

CompletelyDistribLattice (SimpleGraph.Subgraph G)

source

@[simp]

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

default = ⊥

source

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

Inhabited (SimpleGraph.Subgraph G)

source

@[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

source

@[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

source

@[simp]

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

SimpleGraph.Subgraph.neighborSet ⊤ v = SimpleGraph.neighborSet G v

source

@[simp]

theorem SimpleGraph.Subgraph.neighborSet_bot {V : Type u} {G : SimpleGraph V} (v : V) :

SimpleGraph.Subgraph.neighborSet ⊥ v = ∅

source

@[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' : SimpleGraph.Subgraph G) (_ : G' ∈ s), SimpleGraph.Subgraph.neighborSet G' v

source

@[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' : SimpleGraph.Subgraph G) (_ : G' ∈ s), SimpleGraph.Subgraph.neighborSet G' v) ∩ SimpleGraph.neighborSet G v

source

@[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

source

@[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

source

@[simp]

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

SimpleGraph.Subgraph.edgeSet ⊤ = SimpleGraph.edgeSet G

source

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_bot {V : Type u} {G : SimpleGraph V} :

SimpleGraph.Subgraph.edgeSet ⊥ = ∅

source

@[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₂

source

@[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₂

source

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_sSup {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) :

SimpleGraph.Subgraph.edgeSet (sSup s) = ⋃ (G' : SimpleGraph.Subgraph G) (_ : G' ∈ s), SimpleGraph.Subgraph.edgeSet G'

source

@[simp]

theorem SimpleGraph.Subgraph.edgeSet_sInf {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) :

SimpleGraph.Subgraph.edgeSet (sInf s) = (⋂ (G' : SimpleGraph.Subgraph G) (_ : G' ∈ s), SimpleGraph.Subgraph.edgeSet G') ∩ SimpleGraph.edgeSet G

source

@[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)

source

@[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

source

@[simp]

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

SimpleGraph.Subgraph.spanningCoe ⊤ = G

source

@[simp]

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

SimpleGraph.Subgraph.spanningCoe ⊥ = ⊥

source

@[simp]

theorem SimpleGraph.toSubgraph_Adj {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H ≤ G) :

∀ (a a_1 : V), SimpleGraph.Subgraph.Adj (SimpleGraph.toSubgraph H h) a a_1 = SimpleGraph.Adj H a a_1

source

@[simp]

theorem SimpleGraph.toSubgraph_verts {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H ≤ G) :

(SimpleGraph.toSubgraph H h).verts = Set.univ

source

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.

Instances For

source

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'

source

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

SimpleGraph.Subgraph.IsSpanning (SimpleGraph.toSubgraph H h)

source

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'

source

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.

Instances For

source

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.

Instances For

source

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₂

source

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₂)

source

@[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

source

@[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.Adj (SimpleGraph.Subgraph.map f H) a a_1 = Relation.Map H.Adj (↑f) (↑f) a a_1

source

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.

Instances For

source

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)

source

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'

source

@[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.Adj (SimpleGraph.Subgraph.comap f H) u v = (SimpleGraph.Adj G u v ∧ SimpleGraph.Subgraph.Adj H (↑f u) (↑f v))

source

@[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

source

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.

Instances For

source

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)

source

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'

source

@[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

source

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.

Instances For

source

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)

source

@[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

source

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.

Instances For

source

@[simp]

theorem SimpleGraph.Subgraph.coe_hom {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) :

↑(SimpleGraph.Subgraph.hom x) = fun v => ↑v

source

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

Function.Injective ↑(SimpleGraph.Subgraph.hom x)

source

@[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

source

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.

Instances For

source

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

Function.Injective ↑(SimpleGraph.Subgraph.spanningHom x)

source

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

source

instance SimpleGraph.Subgraph.neighborSet.decidablePred {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) [h : DecidableRel G'.Adj] (v : V) :

DecidablePred fun x => x ∈ SimpleGraph.Subgraph.neighborSet G' v

source

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.

source

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.

Instances For

source

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

Fintype ↑(SimpleGraph.Subgraph.neighborSet G' v)

source

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)

source

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') :

Finset.card (Set.toFinset G'.verts) = Fintype.card V

source

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.

Instances For

source

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)] :

Finset.card (Set.toFinset (SimpleGraph.Subgraph.neighborSet G' v)) = SimpleGraph.Subgraph.degree G' v

source

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

source

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

source

@[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

source

@[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

source

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, SimpleGraph.Subgraph.Adj G' v w

Properties of `singletonSubgraph` and `subgraphOfAdj` #

source

instance SimpleGraph.nonempty_singletonSubgraph_verts {V : Type u} {G : SimpleGraph V} (v : V) :

Nonempty ↑(SimpleGraph.singletonSubgraph G v).verts

source

@[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

source

@[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)

source

@[simp]

theorem SimpleGraph.neighborSet_singletonSubgraph {V : Type u} {G : SimpleGraph V} (v : V) (w : V) :

SimpleGraph.Subgraph.neighborSet (SimpleGraph.singletonSubgraph G v) w = ∅

source

@[simp]

theorem SimpleGraph.edgeSet_singletonSubgraph {V : Type u} {G : SimpleGraph V} (v : V) :

SimpleGraph.Subgraph.edgeSet (SimpleGraph.singletonSubgraph G v) = ∅

source

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}

source

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

Nonempty ↑(SimpleGraph.subgraphOfAdj G hvw).verts

source

@[simp]

theorem SimpleGraph.edgeSet_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : SimpleGraph.Adj G v w) :

SimpleGraph.Subgraph.edgeSet (SimpleGraph.subgraphOfAdj G hvw) = {Quotient.mk (Sym2.Rel.setoid V) (v, w)}

source

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

SimpleGraph.subgraphOfAdj G (_ : SimpleGraph.Adj G v w) ≤ H

source

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

SimpleGraph.subgraphOfAdj G (_ : SimpleGraph.Adj G w v) = SimpleGraph.subgraphOfAdj G hvw

source

@[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 : SimpleGraph.Adj G v w) :

SimpleGraph.Subgraph.map f (SimpleGraph.subgraphOfAdj G hvw) = SimpleGraph.subgraphOfAdj G' (_ : SimpleGraph.Adj G' (↑f v) (↑f w))

source

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

SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) u ⊆ {v, w}

source

@[simp]

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

SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) v = {w}

source

@[simp]

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

SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) w = {v}

source

@[simp]

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

SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) u = ∅

source

theorem SimpleGraph.neighborSet_subgraphOfAdj {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (hvw : SimpleGraph.Adj G v w) :

SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅

source

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

SimpleGraph.singletonSubgraph G u ≤ SimpleGraph.subgraphOfAdj G h

source

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

SimpleGraph.singletonSubgraph G v ≤ SimpleGraph.subgraphOfAdj G h

Subgraphs of subgraphs #

source

@[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.

Instances For

source

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

Instances For

source

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.Adj (SimpleGraph.Subgraph.coeSubgraph G'') v w ↔ ∃ hv hw, SimpleGraph.Subgraph.Adj G'' { val := v, property := hv } { val := w, property := hw }

source

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.Adj (SimpleGraph.Subgraph.restrict G'') v w ↔ SimpleGraph.Subgraph.Adj G' ↑v ↑w ∧ SimpleGraph.Subgraph.Adj G'' ↑v ↑w

source

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

source

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

Function.Injective SimpleGraph.Subgraph.coeSubgraph

source

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

source

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 #

source

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.

Induced subgraphs #

source

@[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

source

@[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.Adj (SimpleGraph.Subgraph.induce G' s) u v = (u ∈ s ∧ v ∈ s ∧ SimpleGraph.Subgraph.Adj G' u v)

source

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

Instances For

source

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)

source

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'

source

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

source

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'

source

@[simp]

theorem SimpleGraph.Subgraph.induce_empty {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} :

SimpleGraph.Subgraph.induce G' ∅ = ⊥

source

@[simp]

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

SimpleGraph.Subgraph.induce G' G'.verts = G'

source

theorem SimpleGraph.Subgraph.le_induce_top_verts {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} :

G' ≤ SimpleGraph.Subgraph.induce ⊤ G'.verts

source

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

source

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

source

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

source

theorem SimpleGraph.Subgraph.singletonSubgraph_eq_induce {V : Type u} {G : SimpleGraph V} {v : V} :

SimpleGraph.singletonSubgraph G v = SimpleGraph.Subgraph.induce ⊤ {v}

source

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

SimpleGraph.subgraphOfAdj G hvw = SimpleGraph.Subgraph.induce ⊤ {v, w}

source

@[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.

Instances For

source