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.

def aesop_graph : Lean.ParserDescr

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.

def aesop_graph? : Lean.ParserDescr

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

def aesop_graph_nonterminal : Lean.ParserDescr

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.

structure SimpleGraph (V : Type u) : 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.

• Adj : V → V → Prop

  The adjacency relation of a simple graph.

• symm : Symmetric self.Adj
• loopless : Irreflexive self.Adj

theorem SimpleGraph.ext_iff {V : Type u} {x y : SimpleGraph V} : x = y ↔ x.Adj = y.Adj

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

def SimpleGraph.mk' {V : Type u} : { adj : V → V → Bool // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true } ↪ SimpleGraph V

Constructor for simple graphs using a symmetric irreflexive boolean function.

@[simp]

theorem SimpleGraph.mk'_apply_adj {V : Type u} (x : { adj : V → V → Bool // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true }) (v w : V) : (mk' x).Adj v w = (↑x v w = true)

instance instFintypeSimpleGraphOfDecidableEq {V : Type u} [Fintype V] [DecidableEq V] : Fintype (SimpleGraph V)

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

instance SimpleGraph.instFinite {V : Type u} [Finite V] : Finite (SimpleGraph V)

There are finitely many simple graphs on a given finite type.

def SimpleGraph.fromRel {V : Type u} (r : V → V → Prop) : SimpleGraph V

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

@[simp]

theorem SimpleGraph.fromRel_adj {V : Type u} (r : V → V → Prop) (v w : V) : (fromRel r).Adj v w ↔ v ≠ w ∧ (r v w ∨ r w v)

def completeBipartiteGraph (V : Type u_1) (W : Type u_2) : SimpleGraph (V ⊕ W)

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.

@[simp]

theorem completeBipartiteGraph_adj (V : Type u_1) (W : Type u_2) (v w : V ⊕ W) : (completeBipartiteGraph V W).Adj v w = (v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true)

@[simp]

theorem SimpleGraph.irrefl {V : Type u} (G : SimpleGraph V) {v : V} : ¬G.Adj v v

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

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

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

theorem SimpleGraph.ne_of_adj {V : Type u} (G : SimpleGraph V) {a b : V} (h : G.Adj a b) : a ≠ b

theorem SimpleGraph.Adj.ne {V : Type u} {G : SimpleGraph V} {a b : V} (h : G.Adj a b) : a ≠ b

theorem SimpleGraph.Adj.ne' {V : Type u} {G : SimpleGraph V} {a b : V} (h : G.Adj a b) : b ≠ a

theorem SimpleGraph.ne_of_adj_of_not_adj {V : Type u} (G : SimpleGraph V) {v w x : V} (h : G.Adj v x) (hn : ¬G.Adj w x) : v ≠ w

theorem SimpleGraph.adj_injective {V : Type u} : Function.Injective Adj

@[simp]

theorem SimpleGraph.adj_inj {V : Type u} {G H : SimpleGraph V} : G.Adj = H.Adj ↔ G = H

theorem SimpleGraph.adj_congr_of_sym2 {V : Type u} (G : SimpleGraph V) {u v w x : V} (h : s(u, v) = s(w, x)) : G.Adj u v ↔ G.Adj w x

def SimpleGraph.IsSubgraph {V : Type u} (x y : SimpleGraph V) : Prop

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

instance SimpleGraph.instLE {V : Type u} : LE (SimpleGraph V)

@[simp]

theorem SimpleGraph.isSubgraph_eq_le {V : Type u} : IsSubgraph = fun (x1 x2 : SimpleGraph V) => x1 ≤ x2

instance SimpleGraph.instMax {V : Type u} : Max (SimpleGraph V)

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

@[simp]

theorem SimpleGraph.sup_adj {V : Type u} (x y : SimpleGraph V) (v w : V) : (x ⊔ y).Adj v w ↔ x.Adj v w ∨ y.Adj v w

instance SimpleGraph.instMin {V : Type u} : Min (SimpleGraph V)

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

@[simp]

theorem SimpleGraph.inf_adj {V : Type u} (x y : SimpleGraph V) (v w : V) : (x ⊓ y).Adj v w ↔ x.Adj v w ∧ y.Adj v w

instance SimpleGraph.hasCompl {V : Type u} : HasCompl (SimpleGraph V)

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

@[simp]

theorem SimpleGraph.compl_adj {V : Type u} (G : SimpleGraph V) (v w : V) : Gᶜ.Adj v w ↔ v ≠ w ∧ ¬G.Adj v w

instance SimpleGraph.sdiff {V : Type u} : SDiff (SimpleGraph V)

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

@[simp]

theorem SimpleGraph.sdiff_adj {V : Type u} (x y : SimpleGraph V) (v w : V) : (x \ y).Adj v w ↔ x.Adj v w ∧ ¬y.Adj v w

instance SimpleGraph.supSet {V : Type u} : SupSet (SimpleGraph V)

instance SimpleGraph.infSet {V : Type u} : InfSet (SimpleGraph V)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

instance SimpleGraph.completeAtomicBooleanAlgebra {V : Type u} : CompleteAtomicBooleanAlgebra (SimpleGraph V)

@[reducible, inline]

abbrev SimpleGraph.completeGraph (V : Type u) : SimpleGraph V

The complete graph on a type V is the simple graph with all pairs of distinct vertices.

@[reducible, inline]

abbrev SimpleGraph.emptyGraph (V : Type u) : SimpleGraph V

The graph with no edges on a given vertex type V.

@[simp]

theorem SimpleGraph.top_adj {V : Type u} (v w : V) : ⊤.Adj v w ↔ v ≠ w

@[simp]

theorem SimpleGraph.bot_adj {V : Type u} (v w : V) : ⊥.Adj v w ↔ False

@[simp]

theorem SimpleGraph.completeGraph_eq_top (V : Type u) : completeGraph V = ⊤

@[simp]

theorem SimpleGraph.emptyGraph_eq_bot (V : Type u) : emptyGraph V = ⊥

instance SimpleGraph.instInhabited (V : Type u) : Inhabited (SimpleGraph V)

@[simp]

theorem SimpleGraph.default_def (V : Type u) : default = ⊥

instance SimpleGraph.instUniqueOfSubsingleton {V : Type u} [Subsingleton V] : Unique (SimpleGraph V)

instance SimpleGraph.instNontrivial {V : Type u} [Nontrivial V] : Nontrivial (SimpleGraph V)

instance SimpleGraph.Bot.adjDecidable (V : Type u) : DecidableRel ⊥.Adj

instance SimpleGraph.Sup.adjDecidable (V : Type u) (G H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] : DecidableRel (G ⊔ H).Adj

instance SimpleGraph.Inf.adjDecidable (V : Type u) (G H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] : DecidableRel (G ⊓ H).Adj

instance SimpleGraph.Sdiff.adjDecidable (V : Type u) (G H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] : DecidableRel (G \ H).Adj

instance SimpleGraph.Top.adjDecidable (V : Type u) [DecidableEq V] : DecidableRel ⊤.Adj

instance SimpleGraph.Compl.adjDecidable (V : Type u) (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] : DecidableRel Gᶜ.Adj

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

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

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

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

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

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

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

theorem SimpleGraph.neighborSet_subset_support {V : Type u} (G : SimpleGraph V) (v : V) : G.neighborSet v ⊆ G.support

def SimpleGraph.edgeSetEmbedding (V : Type u_2) : SimpleGraph V ↪o Set (Sym2 V)

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

@[reducible, inline]

abbrev SimpleGraph.edgeSet {V : Type u} (G : SimpleGraph V) : Set (Sym2 V)

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

@[simp]

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

theorem SimpleGraph.not_isDiag_of_mem_edgeSet {V : Type u} (G : SimpleGraph V) {e : Sym2 V} : e ∈ G.edgeSet → ¬e.IsDiag

theorem SimpleGraph.edgeSet_inj {V : Type u} {G₁ G₂ : SimpleGraph V} : G₁.edgeSet = G₂.edgeSet ↔ G₁ = G₂

@[simp]

theorem SimpleGraph.edgeSet_subset_edgeSet {V : Type u} {G₁ G₂ : SimpleGraph V} : G₁.edgeSet ⊆ G₂.edgeSet ↔ G₁ ≤ G₂

@[simp]

theorem SimpleGraph.edgeSet_ssubset_edgeSet {V : Type u} {G₁ G₂ : SimpleGraph V} : G₁.edgeSet ⊂ G₂.edgeSet ↔ G₁ < G₂

theorem SimpleGraph.edgeSet_injective {V : Type u} : Function.Injective edgeSet

theorem SimpleGraph.edgeSet_mono {V : Type u} {G₁ G₂ : SimpleGraph V} : 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₂ : SimpleGraph V} : 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 : SimpleGraph V) : G.edgeSet ⊆ {e : Sym2 V | ¬e.IsDiag}

@[simp]

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

@[simp]

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

@[simp]

theorem SimpleGraph.edgeSet_sdiff {V : Type u} (G₁ G₂ : SimpleGraph V) : (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet

@[simp]

theorem SimpleGraph.disjoint_edgeSet {V : Type u} {G₁ G₂ : SimpleGraph V} : Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂

@[simp]

theorem SimpleGraph.edgeSet_eq_empty {V : Type u} {G : SimpleGraph V} : G.edgeSet = ∅ ↔ G = ⊥

@[simp]

theorem SimpleGraph.edgeSet_nonempty {V : Type u} {G : SimpleGraph V} : G.edgeSet.Nonempty ↔ G ≠ ⊥

@[simp]

theorem SimpleGraph.edgeSet_sdiff_sdiff_isDiag {V : Type u} (G : SimpleGraph V) (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 : SimpleGraph V} {v w : V} : G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.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 : SimpleGraph V} {a b : V} : G.Adj a b ↔ ∃ (e : ↑G.edgeSet), ↑e = s(a, b)

theorem SimpleGraph.edge_other_ne {V : Type u} (G : SimpleGraph V) {e : Sym2 V} (he : e ∈ G.edgeSet) {v : V} (h : v ∈ e) : Sym2.Mem.other h ≠ v

instance SimpleGraph.decidableMemEdgeSet {V : Type u} (G : SimpleGraph V) [DecidableRel G.Adj] : DecidablePred fun (x : Sym2 V) => x ∈ G.edgeSet

instance SimpleGraph.fintypeEdgeSet {V : Type u} (G : SimpleGraph V) [Fintype (Sym2 V)] [DecidableRel G.Adj] : Fintype ↑G.edgeSet

instance SimpleGraph.fintypeEdgeSetBot {V : Type u} : Fintype ↑⊥.edgeSet

instance SimpleGraph.fintypeEdgeSetSup {V : Type u} (G₁ G₂ : SimpleGraph V) [DecidableEq V] [Fintype ↑G₁.edgeSet] [Fintype ↑G₂.edgeSet] : Fintype ↑(G₁ ⊔ G₂).edgeSet

instance SimpleGraph.fintypeEdgeSetInf {V : Type u} (G₁ G₂ : SimpleGraph V) [DecidableEq V] [Fintype ↑G₁.edgeSet] [Fintype ↑G₂.edgeSet] : Fintype ↑(G₁ ⊓ G₂).edgeSet

instance SimpleGraph.fintypeEdgeSetSdiff {V : Type u} (G₁ G₂ : SimpleGraph V) [DecidableEq V] [Fintype ↑G₁.edgeSet] [Fintype ↑G₂.edgeSet] : Fintype ↑(G₁ \ G₂).edgeSet

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

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

instance SimpleGraph.instDecidableRelAdjFromEdgeSetOfDecidablePredSym2MemSetOfDecidableEq {V : Type u} (s : Set (Sym2 V)) [DecidablePred fun (x : Sym2 V) => x ∈ s] [DecidableEq V] : DecidableRel (fromEdgeSet s).Adj

@[simp]

theorem SimpleGraph.fromEdgeSet_adj {V : Type u} {v w : V} (s : Set (Sym2 V)) : (fromEdgeSet s).Adj v w ↔ s(v, w) ∈ s ∧ v ≠ w

@[simp]

theorem SimpleGraph.edgeSet_fromEdgeSet {V : Type u} (s : Set (Sym2 V)) : (fromEdgeSet s).edgeSet = s \ {e : Sym2 V | e.IsDiag}

@[simp]

theorem SimpleGraph.fromEdgeSet_edgeSet {V : Type u} (G : SimpleGraph V) : fromEdgeSet G.edgeSet = G

@[simp]

theorem SimpleGraph.fromEdgeSet_empty {V : Type u} : fromEdgeSet ∅ = ⊥

@[simp]

theorem SimpleGraph.fromEdgeSet_univ {V : Type u} : fromEdgeSet Set.univ = ⊤

@[simp]

theorem SimpleGraph.fromEdgeSet_inter {V : Type u} (s t : Set (Sym2 V)) : fromEdgeSet (s ∩ t) = fromEdgeSet s ⊓ fromEdgeSet t

@[simp]

theorem SimpleGraph.fromEdgeSet_union {V : Type u} (s t : Set (Sym2 V)) : fromEdgeSet (s ∪ t) = fromEdgeSet s ⊔ fromEdgeSet t

@[simp]

theorem SimpleGraph.fromEdgeSet_sdiff {V : Type u} (s t : Set (Sym2 V)) : fromEdgeSet (s \ t) = fromEdgeSet s \ fromEdgeSet t

theorem SimpleGraph.fromEdgeSet_mono {V : Type u} {s t : Set (Sym2 V)} (h : s ⊆ t) : fromEdgeSet s ≤ fromEdgeSet t

@[simp]

theorem SimpleGraph.disjoint_fromEdgeSet {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) : Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet s

@[simp]

theorem SimpleGraph.fromEdgeSet_disjoint {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) : Disjoint (fromEdgeSet s) G ↔ Disjoint s G.edgeSet

instance SimpleGraph.instFintypeElemSym2EdgeSetFromEdgeSetOfDecidableEq {V : Type u} (s : Set (Sym2 V)) [DecidableEq V] [Fintype ↑s] : Fintype ↑(fromEdgeSet s).edgeSet

Incidence set

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

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

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

theorem SimpleGraph.mk'_mem_incidenceSet_iff {V : Type u} (G : SimpleGraph V) {a b 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 : SimpleGraph V) {a b : V} : s(a, b) ∈ G.incidenceSet a ↔ G.Adj a b

theorem SimpleGraph.mk'_mem_incidenceSet_right_iff {V : Type u} (G : SimpleGraph V) {a b : V} : s(a, b) ∈ G.incidenceSet b ↔ G.Adj a b

theorem SimpleGraph.edge_mem_incidenceSet_iff {V : Type u} (G : SimpleGraph V) {a : V} {e : ↑G.edgeSet} : ↑e ∈ G.incidenceSet a ↔ a ∈ ↑e

theorem SimpleGraph.incidenceSet_inter_incidenceSet_subset {V : Type u} (G : SimpleGraph V) {a 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 : SimpleGraph V) {a 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 : SimpleGraph V) {a b : V} {e : Sym2 V} (h : a ≠ b) (ha : e ∈ G.incidenceSet a) (hb : e ∈ G.incidenceSet b) : G.Adj a b

theorem SimpleGraph.incidenceSet_inter_incidenceSet_of_not_adj {V : Type u} (G : SimpleGraph V) {a b : V} (h : ¬G.Adj a b) (hn : a ≠ b) : G.incidenceSet a ∩ G.incidenceSet b = ∅

instance SimpleGraph.decidableMemIncidenceSet {V : Type u} (G : SimpleGraph V) [DecidableEq V] [DecidableRel G.Adj] (v : V) : DecidablePred fun (x : Sym2 V) => x ∈ G.incidenceSet v

@[simp]

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

theorem SimpleGraph.notMem_neighborSet_self {V : Type u} (G : SimpleGraph V) {a : V} : a ∉ G.neighborSet a

@[deprecated SimpleGraph.notMem_neighborSet_self (since := "2025-05-23")]

theorem SimpleGraph.not_mem_neighborSet_self {V : Type u} (G : SimpleGraph V) {a : V} : a ∉ G.neighborSet a

Alias of SimpleGraph.notMem_neighborSet_self.

@[simp]

theorem SimpleGraph.mem_incidenceSet {V : Type u} (G : SimpleGraph V) (v w : V) : s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w

theorem SimpleGraph.mem_incidence_iff_neighbor {V : Type u} (G : SimpleGraph V) {v w : V} : s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v

theorem SimpleGraph.adj_incidenceSet_inter {V : Type u} (G : SimpleGraph V) {v : V} {e : Sym2 V} (he : e ∈ G.edgeSet) (h : v ∈ e) : G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) = {e}

theorem SimpleGraph.compl_neighborSet_disjoint {V : Type u} (G : SimpleGraph V) (v : V) : Disjoint (G.neighborSet v) (Gᶜ.neighborSet v)

theorem SimpleGraph.neighborSet_union_compl_neighborSet_eq {V : Type u} (G : SimpleGraph V) (v : V) : G.neighborSet v ∪ Gᶜ.neighborSet v = {v}ᶜ

theorem SimpleGraph.card_neighborSet_union_compl_neighborSet {V : Type u} [Fintype V] (G : SimpleGraph V) (v : V) [Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)] : (G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset.card = Fintype.card V - 1

theorem SimpleGraph.neighborSet_compl {V : Type u} (G : SimpleGraph V) (v : V) : Gᶜ.neighborSet v = (G.neighborSet v)ᶜ \ {v}

def SimpleGraph.commonNeighbors {V : Type u} (G : SimpleGraph 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.

theorem SimpleGraph.commonNeighbors_eq {V : Type u} (G : SimpleGraph V) (v w : V) : G.commonNeighbors v w = G.neighborSet v ∩ G.neighborSet w

theorem SimpleGraph.mem_commonNeighbors {V : Type u} (G : SimpleGraph V) {u v w : V} : u ∈ G.commonNeighbors v w ↔ G.Adj v u ∧ G.Adj w u

theorem SimpleGraph.commonNeighbors_symm {V : Type u} (G : SimpleGraph V) (v w : V) : G.commonNeighbors v w = G.commonNeighbors w v

theorem SimpleGraph.notMem_commonNeighbors_left {V : Type u} (G : SimpleGraph V) (v w : V) : v ∉ G.commonNeighbors v w

@[deprecated SimpleGraph.notMem_commonNeighbors_left (since := "2025-05-23")]

theorem SimpleGraph.not_mem_commonNeighbors_left {V : Type u} (G : SimpleGraph V) (v w : V) : v ∉ G.commonNeighbors v w

Alias of SimpleGraph.notMem_commonNeighbors_left.

theorem SimpleGraph.notMem_commonNeighbors_right {V : Type u} (G : SimpleGraph V) (v w : V) : w ∉ G.commonNeighbors v w

@[deprecated SimpleGraph.notMem_commonNeighbors_right (since := "2025-05-23")]

theorem SimpleGraph.not_mem_commonNeighbors_right {V : Type u} (G : SimpleGraph V) (v w : V) : w ∉ G.commonNeighbors v w

Alias of SimpleGraph.notMem_commonNeighbors_right.

theorem SimpleGraph.commonNeighbors_subset_neighborSet_left {V : Type u} (G : SimpleGraph V) (v w : V) : G.commonNeighbors v w ⊆ G.neighborSet v

theorem SimpleGraph.commonNeighbors_subset_neighborSet_right {V : Type u} (G : SimpleGraph V) (v w : V) : G.commonNeighbors v w ⊆ G.neighborSet w

instance SimpleGraph.decidableMemCommonNeighbors {V : Type u} (G : SimpleGraph V) [DecidableRel G.Adj] (v w : V) : DecidablePred fun (x : V) => x ∈ G.commonNeighbors v w

theorem SimpleGraph.commonNeighbors_top_eq {V : Type u} {v w : V} : ⊤.commonNeighbors v w = Set.univ \ {v, w}

def SimpleGraph.otherVertexOfIncident {V : Type u} (G : SimpleGraph V) [DecidableEq V] {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.

theorem SimpleGraph.edge_other_incident_set {V : Type u} (G : SimpleGraph V) [DecidableEq V] {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 : SimpleGraph V) [DecidableEq V] {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 : SimpleGraph V) [DecidableEq V] {v w : V} (h : w ∈ G.neighborSet v) : G.otherVertexOfIncident ⋯ = w

def SimpleGraph.incidenceSetEquivNeighborSet {V : Type u} (G : SimpleGraph V) [DecidableEq V] (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.

@[simp]

theorem SimpleGraph.incidenceSetEquivNeighborSet_symm_apply_coe {V : Type u} (G : SimpleGraph V) [DecidableEq V] (v : V) (w : ↑(G.neighborSet v)) : ↑((G.incidenceSetEquivNeighborSet v).symm w) = s(v, ↑w)

@[simp]

theorem SimpleGraph.incidenceSetEquivNeighborSet_apply_coe {V : Type u} (G : SimpleGraph V) [DecidableEq V] (v : V) (e : ↑(G.incidenceSet v)) : ↑((G.incidenceSetEquivNeighborSet v) e) = G.otherVertexOfIncident ⋯