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 : Std.Irrefl self.Adj

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

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

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)

@[implicit_reducible]

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)

@[implicit_reducible]

instance instDecidableRelAdjFromRelOfDecidableEq {V : Type u} [DecidableEq V] (r : V → V → Prop) [DecidableRel r] : DecidableRel (SimpleGraph.fromRel r).Adj

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

instance SimpleGraph.symm_adj {ι : Sort u_1} {V : Type u} (G : SimpleGraph V) (f : ι → V) : Std.Symm fun (i j : ι) => G.Adj (f i) (f j)

@[deprecated "use `≤` instead" (since := "2026-03-25")]

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

@[implicit_reducible]

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

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

theorem SimpleGraph.le_iff_adj {V : Type u} {G H : SimpleGraph V} : G ≤ H ↔ ∀ (v w : V), G.Adj v w → H.Adj v w

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance SimpleGraph.instCompl {V : Type u} : Compl (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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance SimpleGraph.instPartialOrder {V : Type u} : PartialOrder (SimpleGraph V)

@[implicit_reducible]

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

@[implicit_reducible]

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 = ⊥

theorem SimpleGraph.eq_bot_iff_forall_not_adj {V : Type u} {G : SimpleGraph V} : G = ⊥ ↔ ∀ (a b : V), ¬G.Adj a b

theorem SimpleGraph.ne_bot_iff_exists_adj {V : Type u} {G : SimpleGraph V} : G ≠ ⊥ ↔ ∃ (a : V) (b : V), G.Adj a b

theorem SimpleGraph.eq_top_iff_forall_ne_adj {V : Type u} {G : SimpleGraph V} : G = ⊤ ↔ ∀ (a b : V), a ≠ b → G.Adj a b

theorem SimpleGraph.ne_top_iff_exists_not_adj {V : Type u} {G : SimpleGraph V} : G ≠ ⊤ ↔ ∃ (a : V) (b : V), a ≠ b ∧ ¬G.Adj a b

@[implicit_reducible]

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

@[simp]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

theorem SimpleGraph.support_top_of_nontrivial {V : Type u} [Nontrivial V] : ⊤.support = Set.univ

All vertices are in the support of the complete graph if there is more than one vertex.

@[simp]

theorem SimpleGraph.support_bot {V : Type u} : ⊥.support = ∅

The support of the empty graph is empty.

@[simp]

theorem SimpleGraph.support_eq_bot_iff {V : Type u} (G : SimpleGraph V) : G.support = ∅ ↔ G = ⊥

Only the empty graph has empty support.

@[simp]

theorem SimpleGraph.support_of_subsingleton {V : Type u} (G : SimpleGraph V) [Subsingleton V] : G.support = ∅

The support of a graph is empty if there at most one vertex.

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.

@[implicit_reducible]

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

@[simp]

theorem SimpleGraph.not_mem_edgeSet_of_isDiag {V : Type u} (G : SimpleGraph V) {e : Sym2 V} : e.IsDiag → e ∉ G.edgeSet

theorem Sym2.IsDiag.not_mem_edgeSet {V : Type u} (G : SimpleGraph V) {e : Sym2 V} : e.IsDiag → e ∉ G.edgeSet

Alias of SimpleGraph.not_mem_edgeSet_of_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 = Sym2.diagSetᶜ

@[simp]

theorem SimpleGraph.edgeSet_subset_compl_diagSet {V : Type u} (G : SimpleGraph V) : G.edgeSet ⊆ Sym2.diagSetᶜ

@[deprecated SimpleGraph.edgeSet_subset_compl_diagSet (since := "2025-12-10")]

theorem SimpleGraph.edgeSet_subset_setOf_not_isDiag {V : Type u} (G : SimpleGraph V) : G.edgeSet ⊆ Sym2.diagSetᶜ

Alias of SimpleGraph.edgeSet_subset_compl_diagSet.

@[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 \ Sym2.diagSet) = G.edgeSet \ s

This lemma, combined with edgeSet_sdiff and edgeSet_fromEdgeSet, allows proving (G \ fromEdgeSet s).edgeSet = 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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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.

@[implicit_reducible]

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 \ Sym2.diagSet

@[simp]

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

@[simp]

theorem SimpleGraph.fromEdgeSet_le {V : Type u} (G : SimpleGraph V) {s : Set (Sym2 V)} : fromEdgeSet s ≤ G ↔ s \ Sym2.diagSet ⊆ G.edgeSet

theorem SimpleGraph.edgeSet_eq_iff {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) : G.edgeSet = s ↔ G = fromEdgeSet s ∧ Disjoint s Sym2.diagSet

@[simp]

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

@[simp]

theorem SimpleGraph.fromEdgeSet_not_isDiag {V : Type u} : fromEdgeSet Sym2.diagSetᶜ = ⊤

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

@[implicit_reducible]

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

theorem SimpleGraph.disjoint_left {V : Type u} {G H : SimpleGraph V} : Disjoint G H ↔ ∀ (x y : V), G.Adj x y → ¬H.Adj x y

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 = ∅

@[implicit_reducible]

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

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

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

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

@[implicit_reducible]

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

@[simp]

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_apply_coe {V : Type u} (G : SimpleGraph V) [DecidableEq V] (v : V) (e : ↑(G.incidenceSet v)) : ↑((G.incidenceSetEquivNeighborSet v) e) = G.otherVertexOfIncident ⋯

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

def SimpleGraph.IsCompleteBetween {V : Type u} (G : SimpleGraph V) (s t : Set V) : Prop

The condition that the portion of the simple graph G between s and t is complete, that is, every vertex in s is adjacent to every vertex in t, and vice versa.

theorem SimpleGraph.IsCompleteBetween.disjoint {V : Type u} (G : SimpleGraph V) {s t : Set V} (h : G.IsCompleteBetween s t) : Disjoint s t

theorem SimpleGraph.isCompleteBetween_comm {V : Type u} (G : SimpleGraph V) {s t : Set V} : G.IsCompleteBetween s t ↔ G.IsCompleteBetween t s

theorem SimpleGraph.IsCompleteBetween.symm {V : Type u} (G : SimpleGraph V) {s t : Set V} : G.IsCompleteBetween s t → G.IsCompleteBetween t s

Alias of the forward direction of SimpleGraph.isCompleteBetween_comm.

theorem SimpleGraph.subsingleton_iff {V : Type u} : Subsingleton (SimpleGraph V) ↔ Subsingleton V

theorem SimpleGraph.nontrivial_iff {V : Type u} : Nontrivial (SimpleGraph V) ↔ Nontrivial V