# Simple graphs #

This module defines simple graphs on a vertex type V as an irreflexive symmetric relation.

## Main definitions #

• SimpleGraph is a structure for symmetric, irreflexive relations

• SimpleGraph.neighborSet is the Set of vertices adjacent to a given vertex

• SimpleGraph.commonNeighbors is the intersection of the neighbor sets of two given vertices

• SimpleGraph.incidenceSet is the Set of edges containing a given vertex

• CompleteAtomicBooleanAlgebra instance: Under the subgraph relation, SimpleGraph forms a CompleteAtomicBooleanAlgebra. In other words, this is the complete lattice of spanning subgraphs of the complete graph.

## TODO #

• This is the simplest notion of an unoriented graph. This should eventually fit into a more complete combinatorics hierarchy which includes multigraphs and directed graphs. We begin with simple graphs in order to start learning what the combinatorics hierarchy should look like.

A variant of the aesop tactic for use in the graph library. Changes relative to standard aesop:

• We use the SimpleGraph rule set in addition to the default rule sets.
• We instruct Aesop's intro rule to unfold with default transparency.
• We instruct Aesop to fail if it can't fully solve the goal. This allows us to use aesop_graph for auto-params.
Equations
• One or more equations did not get rendered due to their size.
Instances For

Use aesop_graph? to pass along a Try this suggestion when using aesop_graph

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

A variant of aesop_graph which does not fail if it is unable to solve the goal. Use this only for exploration! Nonterminal Aesop is even worse than nonterminal simp.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem SimpleGraph.ext {V : Type u} {x : } {y : } (Adj : x.Adj = y.Adj) :
x = y
theorem SimpleGraph.ext_iff {V : Type u} {x : } {y : } :
structure SimpleGraph (V : Type u) :

A simple graph is an irreflexive symmetric relation Adj on a vertex type V. The relation describes which pairs of vertices are adjacent. There is exactly one edge for every pair of adjacent vertices; see SimpleGraph.edgeSet for the corresponding edge set.

Instances For
theorem SimpleGraph.symm {V : Type u} (self : ) :
theorem SimpleGraph.loopless {V : Type u} (self : ) :
@[simp]
theorem SimpleGraph.mk'_apply_adj {V : Type u} (x : { adj : VVBool // (∀ (x y : V), adj x y = adj y x) ∀ (x : V), ¬adj x x = true }) (v : V) (w : V) :
(SimpleGraph.mk' x).Adj v w = (x v w = true)
def SimpleGraph.mk' {V : Type u} :
{ adj : VVBool // (∀ (x y : V), adj x y = adj y x) ∀ (x : V), ¬adj x x = true }

Constructor for simple graphs using a symmetric irreflexive boolean function.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance instFintypeSimpleGraphOfDecidableEq {V : Type u} [] [] :

We can enumerate simple graphs by enumerating all functions V → V → Bool and filtering on whether they are symmetric and irreflexive.

Equations
• instFintypeSimpleGraphOfDecidableEq = { elems := Finset.map SimpleGraph.mk' Finset.univ, complete := }
def SimpleGraph.fromRel {V : Type u} (r : VVProp) :

Construct the simple graph induced by the given relation. It symmetrizes the relation and makes it irreflexive.

Equations
• = { Adj := fun (a b : V) => a b (r a b r b a), symm := , loopless := }
Instances For
@[simp]
theorem SimpleGraph.fromRel_adj {V : Type u} (r : VVProp) (v : V) (w : V) :
.Adj v w v w (r v w r w v)
def completeGraph (V : Type u) :

The complete graph on a type V is the simple graph with all pairs of distinct vertices adjacent. In Mathlib, this is usually referred to as ⊤.

Equations
• = { Adj := Ne, symm := , loopless := }
Instances For
def emptyGraph (V : Type u) :

The graph with no edges on a given vertex type V. Mathlib prefers the notation ⊥.

Equations
• = { Adj := fun (x x : V) => False, symm := , loopless := }
Instances For
@[simp]
theorem completeBipartiteGraph_adj (V : Type u_1) (W : Type u_2) (v : V W) (w : V W) :
.Adj v w = (v.isLeft = true w.isRight = true v.isRight = true w.isLeft = true)
def completeBipartiteGraph (V : Type u_1) (W : Type u_2) :

Two vertices are adjacent in the complete bipartite graph on two vertex types if and only if they are not from the same side. Any bipartite graph may be regarded as a subgraph of one of these.

Equations
Instances For
@[simp]
theorem SimpleGraph.irrefl {V : Type u} (G : ) {v : V} :
theorem SimpleGraph.adj_comm {V : Type u} (G : ) (u : V) (v : V) :
theorem SimpleGraph.adj_symm {V : Type u} (G : ) {u : V} {v : V} (h : G.Adj u v) :
theorem SimpleGraph.Adj.symm {V : Type u} {G : } {u : V} {v : V} (h : G.Adj u v) :
theorem SimpleGraph.ne_of_adj {V : Type u} (G : ) {a : V} {b : V} (h : G.Adj a b) :
a b
theorem SimpleGraph.Adj.ne {V : Type u} {G : } {a : V} {b : V} (h : G.Adj a b) :
a b
theorem SimpleGraph.Adj.ne' {V : Type u} {G : } {a : V} {b : V} (h : G.Adj a b) :
b a
theorem SimpleGraph.ne_of_adj_of_not_adj {V : Type u} (G : ) {v : V} {w : V} {x : V} (h : G.Adj v x) (hn : ¬G.Adj w x) :
v w
@[simp]
theorem SimpleGraph.adj_inj {V : Type u} {G : } {H : } :
def SimpleGraph.IsSubgraph {V : Type u} (x : ) (y : ) :

The relation that one SimpleGraph is a subgraph of another. Note that this should be spelled ≤.

Equations
• x.IsSubgraph y = ∀ ⦃v w : V⦄, x.Adj v wy.Adj v w
Instances For
instance SimpleGraph.instLE {V : Type u} :
Equations
• SimpleGraph.instLE = { le := SimpleGraph.IsSubgraph }
@[simp]
theorem SimpleGraph.isSubgraph_eq_le {V : Type u} :
SimpleGraph.IsSubgraph = fun (x x_1 : ) => x x_1
instance SimpleGraph.instSup {V : Type u} :

The supremum of two graphs x ⊔ y has edges where either x or y have edges.

Equations
• SimpleGraph.instSup = { sup := fun (x y : ) => { Adj := x.Adj y.Adj, symm := , loopless := } }
@[simp]
theorem SimpleGraph.sup_adj {V : Type u} (x : ) (y : ) (v : V) (w : V) :
instance SimpleGraph.instInf {V : Type u} :

The infimum of two graphs x ⊓ y has edges where both x and y have edges.

Equations
• SimpleGraph.instInf = { inf := fun (x y : ) => { Adj := x.Adj y.Adj, symm := , loopless := } }
@[simp]
theorem SimpleGraph.inf_adj {V : Type u} (x : ) (y : ) (v : V) (w : V) :
instance SimpleGraph.hasCompl {V : Type u} :

We define Gᶜ to be the SimpleGraph V such that no two adjacent vertices in G are adjacent in the complement, and every nonadjacent pair of vertices is adjacent (still ensuring that vertices are not adjacent to themselves).

Equations
• SimpleGraph.hasCompl = { compl := fun (G : ) => { Adj := fun (v w : V) => v w ¬G.Adj v w, symm := , loopless := } }
@[simp]
theorem SimpleGraph.compl_adj {V : Type u} (G : ) (v : V) (w : V) :
instance SimpleGraph.sdiff {V : Type u} :

The difference of two graphs x \ y has the edges of x with the edges of y removed.

Equations
• SimpleGraph.sdiff = { sdiff := fun (x y : ) => { Adj := x.Adj \ y.Adj, symm := , loopless := } }
@[simp]
theorem SimpleGraph.sdiff_adj {V : Type u} (x : ) (y : ) (v : V) (w : V) :
instance SimpleGraph.supSet {V : Type u} :
Equations
• SimpleGraph.supSet = { sSup := fun (s : Set (SimpleGraph V)) => { Adj := fun (a b : V) => Gs, G.Adj a b, symm := , loopless := } }
instance SimpleGraph.infSet {V : Type u} :
Equations
• SimpleGraph.infSet = { sInf := fun (s : Set (SimpleGraph V)) => { Adj := fun (a b : V) => (∀ ⦃G : ⦄, G sG.Adj a b) a b, symm := , loopless := } }
@[simp]
theorem SimpleGraph.sSup_adj {V : Type u} {s : Set (SimpleGraph V)} {a : V} {b : V} :
@[simp]
theorem SimpleGraph.sInf_adj {V : Type u} {a : V} {b : V} {s : Set (SimpleGraph V)} :
@[simp]
theorem SimpleGraph.iSup_adj {ι : Sort u_1} {V : Type u} {a : V} {b : V} {f : ι} :
(⨆ (i : ι), f i).Adj a b ∃ (i : ι), (f i).Adj a b
@[simp]
theorem SimpleGraph.iInf_adj {ι : Sort u_1} {V : Type u} {a : V} {b : V} {f : ι} :
(⨅ (i : ι), f i).Adj a b (∀ (i : ι), (f i).Adj a b) a b
theorem SimpleGraph.sInf_adj_of_nonempty {V : Type u} {a : V} {b : V} {s : Set (SimpleGraph V)} (hs : s.Nonempty) :
theorem SimpleGraph.iInf_adj_of_nonempty {ι : Sort u_1} {V : Type u} {a : V} {b : V} [] {f : ι} :
(⨅ (i : ι), f i).Adj a b ∀ (i : ι), (f i).Adj a b
instance SimpleGraph.distribLattice {V : Type u} :

For graphs G, H, G ≤ H iff ∀ a b, G.Adj a b → H.Adj a b.

Equations
Equations
• SimpleGraph.completeAtomicBooleanAlgebra = let __src := SimpleGraph.distribLattice;
@[simp]
theorem SimpleGraph.top_adj {V : Type u} (v : V) (w : V) :
@[simp]
theorem SimpleGraph.bot_adj {V : Type u} (v : V) (w : V) :
@[simp]
@[simp]
theorem SimpleGraph.instInhabited_default (V : Type u) :
default =
instance SimpleGraph.instInhabited (V : Type u) :
Equations
• = { default := }
Equations
• SimpleGraph.instUniqueOfSubsingleton = { default := , uniq := }
instance SimpleGraph.instNontrivial {V : Type u} [] :
Equations
• =
instance SimpleGraph.Sup.adjDecidable (V : Type u) (G : ) (H : ) [DecidableRel G.Adj] [DecidableRel H.Adj] :
Equations
instance SimpleGraph.Inf.adjDecidable (V : Type u) (G : ) (H : ) [DecidableRel G.Adj] [DecidableRel H.Adj] :
Equations
instance SimpleGraph.Sdiff.adjDecidable (V : Type u) (G : ) (H : ) [DecidableRel G.Adj] [DecidableRel H.Adj] :
Equations
Equations
instance SimpleGraph.Compl.adjDecidable (V : Type u) (G : ) [DecidableRel G.Adj] [] :
Equations
def SimpleGraph.support {V : Type u} (G : ) :
Set V

G.support is the set of vertices that form edges in G.

Equations
Instances For
theorem SimpleGraph.mem_support {V : Type u} (G : ) {v : V} :
v G.support ∃ (w : V), G.Adj v w
theorem SimpleGraph.support_mono {V : Type u} {G : } {G' : } (h : G G') :
G.support G'.support
def SimpleGraph.neighborSet {V : Type u} (G : ) (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}
Instances For
instance SimpleGraph.neighborSet.memDecidable {V : Type u} (G : ) (v : V) [DecidableRel G.Adj] :
DecidablePred fun (x : V) => x G.neighborSet v
Equations

The edges of G consist of the unordered pairs of vertices related by G.Adj. This is the order embedding; for the edge set of a particular graph, see SimpleGraph.edgeSet.

The way edgeSet is defined is such that mem_edgeSet is proved by Iff.rfl. (That is, s(v, w) ∈ G.edgeSet is definitionally equal to G.Adj v w.)

Equations
Instances For
@[reducible, inline]
abbrev SimpleGraph.edgeSet {V : Type u} (G : ) :
Set (Sym2 V)

G.edgeSet is the edge set for G. This is an abbreviation for edgeSetEmbedding G that permits dot notation.

Equations
• G.edgeSet =
Instances For
@[simp]
theorem SimpleGraph.mem_edgeSet {V : Type u} (G : ) {v : V} {w : V} :
s(v, w) G.edgeSet G.Adj v w
theorem SimpleGraph.not_isDiag_of_mem_edgeSet {V : Type u} (G : ) {e : Sym2 V} :
e G.edgeSet¬e.IsDiag
theorem SimpleGraph.edgeSet_inj {V : Type u} {G₁ : } {G₂ : } :
G₁.edgeSet = G₂.edgeSet G₁ = G₂
@[simp]
theorem SimpleGraph.edgeSet_subset_edgeSet {V : Type u} {G₁ : } {G₂ : } :
G₁.edgeSet G₂.edgeSet G₁ G₂
@[simp]
theorem SimpleGraph.edgeSet_ssubset_edgeSet {V : Type u} {G₁ : } {G₂ : } :
G₁.edgeSet G₂.edgeSet G₁ < G₂
theorem SimpleGraph.edgeSet_injective {V : Type u} :
Function.Injective SimpleGraph.edgeSet
theorem SimpleGraph.edgeSet_mono {V : Type u} {G₁ : } {G₂ : } :
G₁ G₂G₁.edgeSet G₂.edgeSet

Alias of the reverse direction of SimpleGraph.edgeSet_subset_edgeSet.

theorem SimpleGraph.edgeSet_strict_mono {V : Type u} {G₁ : } {G₂ : } :
G₁ < G₂G₁.edgeSet G₂.edgeSet

Alias of the reverse direction of SimpleGraph.edgeSet_ssubset_edgeSet.

@[simp]
theorem SimpleGraph.edgeSet_bot {V : Type u} :
.edgeSet =
@[simp]
theorem SimpleGraph.edgeSet_top {V : Type u} :
.edgeSet = {e : Sym2 V | ¬e.IsDiag}
@[simp]
theorem SimpleGraph.edgeSet_subset_setOf_not_isDiag {V : Type u} (G : ) :
G.edgeSet {e : Sym2 V | ¬e.IsDiag}
@[simp]
theorem SimpleGraph.edgeSet_sup {V : Type u} (G₁ : ) (G₂ : ) :
(G₁ G₂).edgeSet = G₁.edgeSet G₂.edgeSet
@[simp]
theorem SimpleGraph.edgeSet_inf {V : Type u} (G₁ : ) (G₂ : ) :
(G₁ G₂).edgeSet = G₁.edgeSet G₂.edgeSet
@[simp]
theorem SimpleGraph.edgeSet_sdiff {V : Type u} (G₁ : ) (G₂ : ) :
(G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet
@[simp]
theorem SimpleGraph.disjoint_edgeSet {V : Type u} {G₁ : } {G₂ : } :
Disjoint G₁.edgeSet G₂.edgeSet Disjoint G₁ G₂
@[simp]
theorem SimpleGraph.edgeSet_eq_empty {V : Type u} {G : } :
G.edgeSet = G =
@[simp]
theorem SimpleGraph.edgeSet_nonempty {V : Type u} {G : } :
G.edgeSet.Nonempty G
@[simp]
theorem SimpleGraph.edgeSet_sdiff_sdiff_isDiag {V : Type u} (G : ) (s : Set (Sym2 V)) :
G.edgeSet \ (s \ {e : Sym2 V | e.IsDiag}) = G.edgeSet \ s

This lemma, combined with edgeSet_sdiff and edgeSet_from_edgeSet, allows proving (G \ from_edgeSet s).edge_set = G.edgeSet \ s by simp.

theorem SimpleGraph.adj_iff_exists_edge {V : Type u} {G : } {v : V} {w : V} :
G.Adj v w v w eG.edgeSet, v e w e

Two vertices are adjacent iff there is an edge between them. The condition v ≠ w ensures they are different endpoints of the edge, which is necessary since when v = w the existential ∃ (e ∈ G.edgeSet), v ∈ e ∧ w ∈ e is satisfied by every edge incident to v.

theorem SimpleGraph.adj_iff_exists_edge_coe {V : Type u} {G : } {a : V} {b : V} :
G.Adj a b ∃ (e : G.edgeSet), e = s(a, b)
theorem SimpleGraph.edge_other_ne {V : Type u} (G : ) {e : Sym2 V} (he : e G.edgeSet) {v : V} (h : v e) :
instance SimpleGraph.decidableMemEdgeSet {V : Type u} (G : ) [DecidableRel G.Adj] :
DecidablePred fun (x : Sym2 V) => x G.edgeSet
Equations
• G.decidableMemEdgeSet =
instance SimpleGraph.fintypeEdgeSet {V : Type u} (G : ) [Fintype (Sym2 V)] [DecidableRel G.Adj] :
Fintype G.edgeSet
Equations
instance SimpleGraph.fintypeEdgeSetBot {V : Type u} :
Fintype .edgeSet
Equations
• SimpleGraph.fintypeEdgeSetBot = .mpr inferInstance
instance SimpleGraph.fintypeEdgeSetSup {V : Type u} (G₁ : ) (G₂ : ) [] [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
Fintype (G₁ G₂).edgeSet
Equations
• G₁.fintypeEdgeSetSup G₂ = .mpr inferInstance
instance SimpleGraph.fintypeEdgeSetInf {V : Type u} (G₁ : ) (G₂ : ) [] [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
Fintype (G₁ G₂).edgeSet
Equations
• G₁.fintypeEdgeSetInf G₂ = .mpr (G₁.edgeSet.fintypeInter G₂.edgeSet)
instance SimpleGraph.fintypeEdgeSetSdiff {V : Type u} (G₁ : ) (G₂ : ) [] [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
Fintype (G₁ \ G₂).edgeSet
Equations
• G₁.fintypeEdgeSetSdiff G₂ = .mpr (G₁.edgeSet.fintypeDiff G₂.edgeSet)
def SimpleGraph.fromEdgeSet {V : Type u} (s : Set (Sym2 V)) :

fromEdgeSet constructs a SimpleGraph from a set of edges, without loops.

Equations
• = { Adj := Ne, symm := , loopless := }
Instances For
@[simp]
theorem SimpleGraph.fromEdgeSet_adj {V : Type u} {v : V} {w : V} (s : Set (Sym2 V)) :
.Adj v w s(v, w) s v w
@[simp]
theorem SimpleGraph.edgeSet_fromEdgeSet {V : Type u} (s : Set (Sym2 V)) :
.edgeSet = s \ {e : Sym2 V | e.IsDiag}
@[simp]
@[simp]
@[simp]
theorem SimpleGraph.fromEdgeSet_inter {V : Type u} (s : Set (Sym2 V)) (t : Set (Sym2 V)) :
@[simp]
theorem SimpleGraph.fromEdgeSet_union {V : Type u} (s : Set (Sym2 V)) (t : Set (Sym2 V)) :
@[simp]
theorem SimpleGraph.fromEdgeSet_sdiff {V : Type u} (s : Set (Sym2 V)) (t : Set (Sym2 V)) :
theorem SimpleGraph.fromEdgeSet_mono {V : Type u} {s : Set (Sym2 V)} {t : Set (Sym2 V)} (h : s t) :
@[simp]
theorem SimpleGraph.disjoint_fromEdgeSet {V : Type u} (G : ) (s : Set (Sym2 V)) :
Disjoint G.edgeSet s
@[simp]
theorem SimpleGraph.fromEdgeSet_disjoint {V : Type u} (G : ) (s : Set (Sym2 V)) :
Disjoint s G.edgeSet
Equations
• = .mpr inferInstance

### Incidence set #

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

Set of edges incident to a given vertex, aka incidence set.

Equations
Instances For
theorem SimpleGraph.incidenceSet_subset {V : Type u} (G : ) (v : V) :
G.incidenceSet v G.edgeSet
theorem SimpleGraph.mk'_mem_incidenceSet_iff {V : Type u} (G : ) {a : V} {b : V} {c : V} :
s(b, c) G.incidenceSet a G.Adj b c (a = b a = c)
theorem SimpleGraph.mk'_mem_incidenceSet_left_iff {V : Type u} (G : ) {a : V} {b : V} :
s(a, b) G.incidenceSet a G.Adj a b
theorem SimpleGraph.mk'_mem_incidenceSet_right_iff {V : Type u} (G : ) {a : V} {b : V} :
s(a, b) G.incidenceSet b G.Adj a b
theorem SimpleGraph.edge_mem_incidenceSet_iff {V : Type u} (G : ) {a : V} {e : G.edgeSet} :
e G.incidenceSet a a e
theorem SimpleGraph.incidenceSet_inter_incidenceSet_subset {V : Type u} (G : ) {a : V} {b : V} (h : a b) :
G.incidenceSet a G.incidenceSet b {s(a, b)}
theorem SimpleGraph.incidenceSet_inter_incidenceSet_of_adj {V : Type u} (G : ) {a : V} {b : V} (h : G.Adj a b) :
G.incidenceSet a G.incidenceSet b = {s(a, b)}
theorem SimpleGraph.adj_of_mem_incidenceSet {V : Type u} (G : ) {a : V} {b : V} {e : Sym2 V} (h : a b) (ha : e G.incidenceSet a) (hb : e G.incidenceSet b) :
theorem SimpleGraph.incidenceSet_inter_incidenceSet_of_not_adj {V : Type u} (G : ) {a : V} {b : V} (h : ¬G.Adj a b) (hn : a b) :
G.incidenceSet a G.incidenceSet b =
instance SimpleGraph.decidableMemIncidenceSet {V : Type u} (G : ) [] [DecidableRel G.Adj] (v : V) :
DecidablePred fun (x : Sym2 V) => x G.incidenceSet v
Equations
@[simp]
theorem SimpleGraph.mem_neighborSet {V : Type u} (G : ) (v : V) (w : V) :
w G.neighborSet v G.Adj v w
theorem SimpleGraph.not_mem_neighborSet_self {V : Type u} (G : ) {a : V} :
aG.neighborSet a
@[simp]
theorem SimpleGraph.mem_incidenceSet {V : Type u} (G : ) (v : V) (w : V) :
s(v, w) G.incidenceSet v G.Adj v w
theorem SimpleGraph.mem_incidence_iff_neighbor {V : Type u} (G : ) {v : V} {w : V} :
s(v, w) G.incidenceSet v w G.neighborSet v
theorem SimpleGraph.adj_incidenceSet_inter {V : Type u} (G : ) {v : V} {e : Sym2 V} (he : e G.edgeSet) (h : v e) :
G.incidenceSet v G.incidenceSet = {e}
theorem SimpleGraph.compl_neighborSet_disjoint {V : Type u} (G : ) (v : V) :
Disjoint (G.neighborSet v) (G.neighborSet v)
theorem SimpleGraph.neighborSet_union_compl_neighborSet_eq {V : Type u} (G : ) (v : V) :
G.neighborSet v G.neighborSet v = {v}
theorem SimpleGraph.card_neighborSet_union_compl_neighborSet {V : Type u} [] (G : ) (v : V) [Fintype (G.neighborSet v G.neighborSet v)] :
(G.neighborSet v G.neighborSet v).toFinset.card =
theorem SimpleGraph.neighborSet_compl {V : Type u} (G : ) (v : V) :
G.neighborSet v = (G.neighborSet v) \ {v}
def SimpleGraph.commonNeighbors {V : Type u} (G : ) (v : V) (w : V) :
Set V

The set of common neighbors between two vertices v and w in a graph G is the intersection of the neighbor sets of v and w.

Equations
• G.commonNeighbors v w = G.neighborSet v G.neighborSet w
Instances For
theorem SimpleGraph.commonNeighbors_eq {V : Type u} (G : ) (v : V) (w : V) :
G.commonNeighbors v w = G.neighborSet v G.neighborSet w
theorem SimpleGraph.mem_commonNeighbors {V : Type u} (G : ) {u : V} {v : V} {w : V} :
theorem SimpleGraph.commonNeighbors_symm {V : Type u} (G : ) (v : V) (w : V) :
G.commonNeighbors v w = G.commonNeighbors w v
theorem SimpleGraph.not_mem_commonNeighbors_left {V : Type u} (G : ) (v : V) (w : V) :
vG.commonNeighbors v w
theorem SimpleGraph.not_mem_commonNeighbors_right {V : Type u} (G : ) (v : V) (w : V) :
wG.commonNeighbors v w
theorem SimpleGraph.commonNeighbors_subset_neighborSet_left {V : Type u} (G : ) (v : V) (w : V) :
G.commonNeighbors v w G.neighborSet v
theorem SimpleGraph.commonNeighbors_subset_neighborSet_right {V : Type u} (G : ) (v : V) (w : V) :
G.commonNeighbors v w G.neighborSet w
instance SimpleGraph.decidableMemCommonNeighbors {V : Type u} (G : ) [DecidableRel G.Adj] (v : V) (w : V) :
DecidablePred fun (x : V) => x G.commonNeighbors v w
Equations
theorem SimpleGraph.commonNeighbors_top_eq {V : Type u} {v : V} {w : V} :
.commonNeighbors v w = Set.univ \ {v, w}
def SimpleGraph.otherVertexOfIncident {V : Type u} (G : ) [] {v : V} {e : Sym2 V} (h : e G.incidenceSet v) :
V

Given an edge incident to a particular vertex, get the other vertex on the edge.

Equations
• G.otherVertexOfIncident h =
Instances For
theorem SimpleGraph.edge_other_incident_set {V : Type u} (G : ) [] {v : V} {e : Sym2 V} (h : e G.incidenceSet v) :
e G.incidenceSet (G.otherVertexOfIncident h)
theorem SimpleGraph.incidence_other_prop {V : Type u} (G : ) [] {v : V} {e : Sym2 V} (h : e G.incidenceSet v) :
G.otherVertexOfIncident h G.neighborSet v
theorem SimpleGraph.incidence_other_neighbor_edge {V : Type u} (G : ) [] {v : V} {w : V} (h : w G.neighborSet v) :
G.otherVertexOfIncident = w
@[simp]
theorem SimpleGraph.incidenceSetEquivNeighborSet_symm_apply_coe {V : Type u} (G : ) [] (v : V) (w : (G.neighborSet v)) :
((G.incidenceSetEquivNeighborSet v).symm w) = s(v, w)
@[simp]
theorem SimpleGraph.incidenceSetEquivNeighborSet_apply_coe {V : Type u} (G : ) [] (v : V) (e : (G.incidenceSet v)) :
((G.incidenceSetEquivNeighborSet v) e) = G.otherVertexOfIncident
def SimpleGraph.incidenceSetEquivNeighborSet {V : Type u} (G : ) [] (v : V) :
(G.incidenceSet v) (G.neighborSet v)

There is an equivalence between the set of edges incident to a given vertex and the set of vertices adjacent to the vertex.

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

## Edge deletion #

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

Given a set of vertex pairs, remove all of the corresponding edges from the graph's edge set, if present.

See also: SimpleGraph.Subgraph.deleteEdges.

Equations
• G.deleteEdges s =
Instances For
@[simp]
theorem SimpleGraph.deleteEdges_adj {V : Type u} {G : } {v : V} {w : V} {s : Set (Sym2 V)} :
@[simp]
theorem SimpleGraph.deleteEdges_edgeSet {V : Type u} (G : ) (G' : ) :
G.deleteEdges G'.edgeSet = G \ G'
@[simp]
theorem SimpleGraph.deleteEdges_deleteEdges {V : Type u} {G : } (s : Set (Sym2 V)) (s' : Set (Sym2 V)) :
(G.deleteEdges s).deleteEdges s' = G.deleteEdges (s s')
@[simp]
theorem SimpleGraph.deleteEdges_empty {V : Type u} {G : } :
G.deleteEdges = G
@[simp]
theorem SimpleGraph.deleteEdges_univ {V : Type u} {G : } :
G.deleteEdges Set.univ =
theorem SimpleGraph.deleteEdges_le {V : Type u} {G : } (s : Set (Sym2 V)) :
G.deleteEdges s G
theorem SimpleGraph.deleteEdges_anti {V : Type u} {G : } {s₁ : Set (Sym2 V)} {s₂ : Set (Sym2 V)} (h : s₁ s₂) :
G.deleteEdges s₂ G.deleteEdges s₁
theorem SimpleGraph.deleteEdges_mono {V : Type u} {G : } {H : } {s : Set (Sym2 V)} (h : G H) :
G.deleteEdges s H.deleteEdges s
@[simp]
theorem SimpleGraph.deleteEdges_eq_self {V : Type u} {G : } {s : Set (Sym2 V)} :
G.deleteEdges s = G Disjoint G.edgeSet s
theorem SimpleGraph.deleteEdges_eq_inter_edgeSet {V : Type u} {G : } (s : Set (Sym2 V)) :
G.deleteEdges s = G.deleteEdges (s G.edgeSet)
theorem SimpleGraph.deleteEdges_sdiff_eq_of_le {V : Type u} {G : } {H : } (h : H G) :
G.deleteEdges (G.edgeSet \ H.edgeSet) = H
theorem SimpleGraph.edgeSet_deleteEdges {V : Type u} {G : } (s : Set (Sym2 V)) :
(G.deleteEdges s).edgeSet = G.edgeSet \ s