mathlib documentation

combinatorics.simple_graph.basic

Simple graphs #

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

There is a basic API for locally finite graphs and for graphs with finitely many vertices.

Main definitions #

Notations #

Implementation notes #

Naming Conventions #

Todo #

source
theorem simple_graph.ext {V : Type u} (x y : simple_graph V) (h : x.adj = y.adj) :
x = y
source
theorem simple_graph.ext_iff {V : Type u} (x y : simple_graph V) :
x = y ↔ x.adj = y.adj
source
@[ext]
structure simple_graph (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 simple_graph.edge_set for the corresponding edge set.

Instances for simple_graph
source
@[protected, instance]
noncomputable def simple_graph.fintype {V : Type u} [fintype V] :
fintype (simple_graph V)
Equations
source
def simple_graph.from_rel {V : Type u} (r : V → V → Prop) :
simple_graph V

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

Equations
source
@[simp]
theorem simple_graph.from_rel_adj {V : Type u} (r : V → V → Prop) (v w : V) :
(simple_graph.from_rel r).adj v w ↔ v ≠ w ∧ (r v w ∨ r w v)
source
def complete_graph (V : Type u) :
simple_graph V

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
source
def empty_graph (V : Type u) :
simple_graph V

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

Equations
source
def complete_bipartite_graph (V : Type u_1) (W : Type u_2) :
simple_graph (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. Bipartite graphs in general may be regarded as being subgraphs of one of these.

TODO also introduce complete multi-partite graphs, where the vertex type is a sigma type of an indexed family of vertex types

Equations
source
@[simp]
theorem complete_bipartite_graph_adj (V : Type u_1) (W : Type u_2) (v w : V ⊕ W) :
(complete_bipartite_graph V W).adj v w = (↥(v.is_left) ∧ ↥(w.is_right) ∨ ↥(v.is_right) ∧ ↥(w.is_left))
source
@[protected, simp]
theorem simple_graph.irrefl {V : Type u} (G : simple_graph V) {v : V} :
¬G.adj v v
source
theorem simple_graph.adj_comm {V : Type u} (G : simple_graph V) (u v : V) :
G.adj u v ↔ G.adj v u
source
@[symm]
theorem simple_graph.adj_symm {V : Type u} (G : simple_graph V) {u v : V} (h : G.adj u v) :
G.adj v u
source
theorem simple_graph.adj.symm {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
G.adj v u
source
theorem simple_graph.ne_of_adj {V : Type u} (G : simple_graph V) {a b : V} (h : G.adj a b) :
a ≠ b
source
@[protected]
theorem simple_graph.adj.ne {V : Type u} {G : simple_graph V} {a b : V} (h : G.adj a b) :
a ≠ b
source
@[protected]
theorem simple_graph.adj.ne' {V : Type u} {G : simple_graph V} {a b : V} (h : G.adj a b) :
b ≠ a
source
theorem simple_graph.ne_of_adj_of_not_adj {V : Type u} (G : simple_graph V) {v w x : V} (h : G.adj v x) (hn : ¬G.adj w x) :
v ≠ w
source
def simple_graph.is_subgraph {V : Type u} (x y : simple_graph V) :
Prop

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

Equations
source
@[protected, instance]
def simple_graph.has_le {V : Type u} :
has_le (simple_graph V)
Equations
source
@[simp]
theorem simple_graph.is_subgraph_eq_le {V : Type u} :
simple_graph.is_subgraph = has_le.le
source
@[protected, instance]
def simple_graph.has_sup {V : Type u} :
has_sup (simple_graph V)

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

Equations
source
@[simp]
theorem simple_graph.sup_adj {V : Type u} (x y : simple_graph V) (v w : V) :
(x ⊔ y).adj v w ↔ x.adj v w ∨ y.adj v w
source
@[protected, instance]
def simple_graph.has_inf {V : Type u} :
has_inf (simple_graph V)

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

Equations
source
@[simp]
theorem simple_graph.inf_adj {V : Type u} (x y : simple_graph V) (v w : V) :
(x ⊓ y).adj v w ↔ x.adj v w ∧ y.adj v w
source
@[protected, instance]
def simple_graph.has_compl {V : Type u} :
has_compl (simple_graph V)

We define Gᶜ to be the simple_graph 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
source
@[simp]
theorem simple_graph.compl_adj {V : Type u} (G : simple_graph V) (v w : V) :
Gᶜ.adj v w ↔ v ≠ w ∧ ¬G.adj v w
source
@[protected, instance]
def simple_graph.has_sdiff {V : Type u} :
has_sdiff (simple_graph V)

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

Equations
source
@[simp]
theorem simple_graph.sdiff_adj {V : Type u} (x y : simple_graph V) (v w : V) :
(x \ y).adj v w ↔ x.adj v w ∧ ¬y.adj v w
source
@[protected, instance]
def simple_graph.boolean_algebra {V : Type u} :
boolean_algebra (simple_graph V)
Equations
source
@[simp]
theorem simple_graph.top_adj {V : Type u} (v w : V) :
⊤.adj v w ↔ v ≠ w
source
@[simp]
theorem simple_graph.bot_adj {V : Type u} (v w : V) :
⊥.adj v w ↔ false
source
@[simp]
theorem simple_graph.complete_graph_eq_top (V : Type u) :
complete_graph V = ⊤
source
@[simp]
theorem simple_graph.empty_graph_eq_bot (V : Type u) :
empty_graph V = ⊥
source
@[protected, instance]
def simple_graph.inhabited (V : Type u) :
inhabited (simple_graph V)
Equations
source
@[simp]
theorem simple_graph.inhabited_default (V : Type u) :
inhabited.default = ⊥
source
@[protected, instance]
def simple_graph.bot.adj_decidable (V : Type u) :
decidable_rel ⊥.adj
Equations
source
@[protected, instance]
def simple_graph.sup.adj_decidable (V : Type u) (G H : simple_graph V) [decidable_rel G.adj] [decidable_rel H.adj] :
decidable_rel (G ⊔ H).adj
Equations
source
@[protected, instance]
def simple_graph.inf.adj_decidable (V : Type u) (G H : simple_graph V) [decidable_rel G.adj] [decidable_rel H.adj] :
decidable_rel (G ⊓ H).adj
Equations
source
@[protected, instance]
def simple_graph.sdiff.adj_decidable (V : Type u) (G H : simple_graph V) [decidable_rel G.adj] [decidable_rel H.adj] :
decidable_rel (G \ H).adj
Equations
source
@[protected, instance]
def simple_graph.top.adj_decidable (V : Type u) [decidable_eq V] :
decidable_rel ⊤.adj
Equations
source
@[protected, instance]
def simple_graph.compl.adj_decidable (V : Type u) (G : simple_graph V) [decidable_rel G.adj] [decidable_eq V] :
decidable_rel Gᶜ.adj
Equations
source
def simple_graph.support {V : Type u} (G : simple_graph V) :
set V

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

Equations
source
theorem simple_graph.mem_support {V : Type u} (G : simple_graph V) {v : V} :
v ∈ G.support ↔ ∃ (w : V), G.adj v w
source
theorem simple_graph.support_mono {V : Type u} {G G' : simple_graph V} (h : G ≤ G') :
G.support ⊆ G'.support
source
def simple_graph.neighbor_set {V : Type u} (G : simple_graph V) (v : V) :
set V

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

Equations
Instances for ↥simple_graph.neighbor_set
source
@[protected, instance]
def simple_graph.neighbor_set.mem_decidable {V : Type u} (G : simple_graph V) (v : V) [decidable_rel G.adj] :
decidable_pred (λ (_x : V), _x ∈ G.neighbor_set v)
Equations
source
def simple_graph.edge_set {V : Type u} :
simple_graph V ↪o set (sym2 V)

The edges of G consist of the unordered pairs of vertices related by G.adj.

The way edge_set is defined is such that mem_edge_set is proved by refl. (That is, ⟦(v, w)⟧ ∈ G.edge_set is definitionally equal to G.adj v w.)

Equations
source
@[simp]
theorem simple_graph.mem_edge_set {V : Type u} (G : simple_graph V) {v w : V} :
⟦(v, w)⟧ ∈ ⇑simple_graph.edge_set G ↔ G.adj v w
source
theorem simple_graph.not_is_diag_of_mem_edge_set {V : Type u} (G : simple_graph V) {e : sym2 V} :
e ∈ ⇑simple_graph.edge_set G → ¬e.is_diag
source
@[simp]
theorem simple_graph.edge_set_inj {V : Type u} {G₁ G₂ : simple_graph V} :
⇑simple_graph.edge_set G₁ = ⇑simple_graph.edge_set G₂ ↔ G₁ = G₂
source
@[simp]
theorem simple_graph.edge_set_subset_edge_set {V : Type u} {G₁ G₂ : simple_graph V} :
⇑simple_graph.edge_set G₁ ⊆ ⇑simple_graph.edge_set G₂ ↔ G₁ ≤ G₂
source
@[simp]
theorem simple_graph.edge_set_ssubset_edge_set {V : Type u} {G₁ G₂ : simple_graph V} :
⇑simple_graph.edge_set G₁ ⊂ ⇑simple_graph.edge_set G₂ ↔ G₁ < G₂
source
theorem simple_graph.edge_set_injective {V : Type u} :
function.injective ⇑simple_graph.edge_set
source
theorem simple_graph.edge_set_mono {V : Type u} {G₁ G₂ : simple_graph V} :
G₁ ≤ G₂ → ⇑simple_graph.edge_set G₁ ⊆ ⇑simple_graph.edge_set G₂

Alias of the reverse direction of simple_graph.edge_set_subset_edge_set.

source
theorem simple_graph.edge_set_strict_mono {V : Type u} {G₁ G₂ : simple_graph V} :
G₁ < G₂ → ⇑simple_graph.edge_set G₁ ⊂ ⇑simple_graph.edge_set G₂

Alias of the reverse direction of simple_graph.edge_set_ssubset_edge_set.

source
@[simp]
theorem simple_graph.edge_set_bot {V : Type u} :
⇑simple_graph.edge_set ⊥ = ∅
source
@[simp]
theorem simple_graph.edge_set_sup {V : Type u} (G₁ G₂ : simple_graph V) :
⇑simple_graph.edge_set (G₁ ⊔ G₂) = ⇑simple_graph.edge_set G₁ ∪ ⇑simple_graph.edge_set G₂
source
@[simp]
theorem simple_graph.edge_set_inf {V : Type u} (G₁ G₂ : simple_graph V) :
⇑simple_graph.edge_set (G₁ ⊓ G₂) = ⇑simple_graph.edge_set G₁ ∩ ⇑simple_graph.edge_set G₂
source
@[simp]
theorem simple_graph.edge_set_sdiff {V : Type u} (G₁ G₂ : simple_graph V) :
⇑simple_graph.edge_set (G₁ \ G₂) = ⇑simple_graph.edge_set G₁ \ ⇑simple_graph.edge_set G₂
source
@[simp]
theorem simple_graph.edge_set_sdiff_sdiff_is_diag {V : Type u} (G : simple_graph V) (s : set (sym2 V)) :
⇑simple_graph.edge_set G \ (s \ {e : sym2 V | e.is_diag}) = ⇑simple_graph.edge_set G \ s

This lemma, combined with edge_set_sdiff and edge_set_from_edge_set, allows proving (G \ from_edge_set s).edge_set = G.edge_set \ s by simp.

source
theorem simple_graph.adj_iff_exists_edge {V : Type u} (G : simple_graph V) {v w : V} :
G.adj v w ↔ v ≠ w ∧ ∃ (e : sym2 V) (H : e ∈ ⇑simple_graph.edge_set G), 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.edge_set), v ∈ e ∧ w ∈ e is satisfied by every edge incident to v.

source
theorem simple_graph.adj_iff_exists_edge_coe {V : Type u} (G : simple_graph V) {a b : V} :
G.adj a b ↔ ∃ (e : ↥(⇑simple_graph.edge_set G)), ↑e = ⟦(a, b)⟧
source
theorem simple_graph.edge_other_ne {V : Type u} (G : simple_graph V) {e : sym2 V} (he : e ∈ ⇑simple_graph.edge_set G) {v : V} (h : v ∈ e) :
sym2.mem.other h ≠ v
source
@[protected, instance]
def simple_graph.decidable_mem_edge_set {V : Type u} (G : simple_graph V) [decidable_rel G.adj] :
decidable_pred (λ (_x : sym2 V), _x ∈ ⇑simple_graph.edge_set G)
Equations
source
@[protected, instance]
def simple_graph.fintype_edge_set {V : Type u} (G : simple_graph V) [decidable_eq V] [fintype V] [decidable_rel G.adj] :
fintype ↥(⇑simple_graph.edge_set G)
Equations
source
@[protected, instance]
def simple_graph.fintype_edge_set_bot {V : Type u} :
fintype ↥(⇑simple_graph.edge_set ⊥)
Equations
source
@[protected, instance]
def simple_graph.fintype_edge_set_sup {V : Type u} (G₁ G₂ : simple_graph V) [decidable_eq V] [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] :
fintype ↥(⇑simple_graph.edge_set (G₁ ⊔ G₂))
Equations
source
@[protected, instance]
def simple_graph.fintype_edge_set_inf {V : Type u} (G₁ G₂ : simple_graph V) [decidable_eq V] [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] :
fintype ↥(⇑simple_graph.edge_set (G₁ ⊓ G₂))
Equations
source
@[protected, instance]
def simple_graph.fintype_edge_set_sdiff {V : Type u} (G₁ G₂ : simple_graph V) [decidable_eq V] [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] :
fintype ↥(⇑simple_graph.edge_set (G₁ \ G₂))
Equations
source
def simple_graph.from_edge_set {V : Type u} (s : set (sym2 V)) :
simple_graph V

from_edge_set constructs a simple_graph from a set of edges, without loops.

Equations
source
@[simp]
theorem simple_graph.from_edge_set_adj {V : Type u} {v w : V} (s : set (sym2 V)) :
(simple_graph.from_edge_set s).adj v w ↔ ⟦(v, w)⟧ ∈ s ∧ v ≠ w
source
@[simp]
theorem simple_graph.edge_set_from_edge_set {V : Type u} (s : set (sym2 V)) :
⇑simple_graph.edge_set (simple_graph.from_edge_set s) = s \ {e : sym2 V | e.is_diag}
source
@[simp]
theorem simple_graph.from_edge_set_edge_set {V : Type u} (G : simple_graph V) :
simple_graph.from_edge_set (⇑simple_graph.edge_set G) = G
source
@[simp]
theorem simple_graph.from_edge_set_empty {V : Type u} :
simple_graph.from_edge_set ∅ = ⊥
source
@[simp]
theorem simple_graph.from_edge_set_univ {V : Type u} :
simple_graph.from_edge_set set.univ = ⊤
source
@[simp]
theorem simple_graph.from_edge_set_inf {V : Type u} (s t : set (sym2 V)) :
simple_graph.from_edge_set s ⊓ simple_graph.from_edge_set t = simple_graph.from_edge_set (s ∩ t)
source
@[simp]
theorem simple_graph.from_edge_set_sup {V : Type u} (s t : set (sym2 V)) :
simple_graph.from_edge_set s ⊔ simple_graph.from_edge_set t = simple_graph.from_edge_set (s ∪ t)
source
@[simp]
theorem simple_graph.from_edge_set_sdiff {V : Type u} (s t : set (sym2 V)) :
simple_graph.from_edge_set s \ simple_graph.from_edge_set t = simple_graph.from_edge_set (s \ t)
source
theorem simple_graph.from_edge_set_mono {V : Type u} {s t : set (sym2 V)} (h : s ⊆ t) :
simple_graph.from_edge_set s ≤ simple_graph.from_edge_set t
source
@[protected, instance]
def simple_graph.edge_set.fintype {V : Type u} (s : set (sym2 V)) [decidable_eq V] [fintype ↥s] :
fintype ↥(⇑simple_graph.edge_set (simple_graph.from_edge_set s))
Equations

Darts #

source
theorem simple_graph.dart.ext_iff {V : Type u} {G : simple_graph V} (x y : G.dart) :
x = y ↔ x.to_prod = y.to_prod
source
theorem simple_graph.dart.ext {V : Type u} {G : simple_graph V} (x y : G.dart) (h : x.to_prod = y.to_prod) :
x = y
source
@[ext]
structure simple_graph.dart {V : Type u} (G : simple_graph V) :
Type u

A dart is an oriented edge, implemented as an ordered pair of adjacent vertices. This terminology comes from combinatorial maps, and they are also known as "half-edges" or "bonds."

Instances for simple_graph.dart
source
@[protected, instance]
def simple_graph.dart.decidable_eq {V : Type u} [a : decidable_eq V] (G : simple_graph V) :
decidable_eq G.dart
source
@[reducible]
def simple_graph.dart.fst {V : Type u} {G : simple_graph V} (d : G.dart) :
V

The first vertex for the dart.

source
@[reducible]
def simple_graph.dart.snd {V : Type u} {G : simple_graph V} (d : G.dart) :
V

The second vertex for the dart.

source
theorem simple_graph.dart.to_prod_injective {V : Type u} {G : simple_graph V} :
function.injective simple_graph.dart.to_prod
source
@[protected, instance]
def simple_graph.dart.fintype {V : Type u} {G : simple_graph V} [fintype V] [decidable_rel G.adj] :
fintype G.dart
Equations
source
def simple_graph.dart.edge {V : Type u} {G : simple_graph V} (d : G.dart) :
sym2 V

The edge associated to the dart.

Equations
source
@[simp]
theorem simple_graph.dart.edge_mk {V : Type u} {G : simple_graph V} {p : V × V} (h : G.adj p.fst p.snd) :
{to_prod := p, is_adj := h}.edge = ⟦p⟧
source
@[simp]
theorem simple_graph.dart.edge_mem {V : Type u} {G : simple_graph V} (d : G.dart) :
d.edge ∈ ⇑simple_graph.edge_set G
source
@[simp]
theorem simple_graph.dart.symm_to_prod {V : Type u} {G : simple_graph V} (d : G.dart) :
d.symm.to_prod = d.to_prod.swap
source
def simple_graph.dart.symm {V : Type u} {G : simple_graph V} (d : G.dart) :
G.dart

The dart with reversed orientation from a given dart.

Equations
source
@[simp]
theorem simple_graph.dart.symm_mk {V : Type u} {G : simple_graph V} {p : V × V} (h : G.adj p.fst p.snd) :
{to_prod := p, is_adj := h}.symm = {to_prod := p.swap, is_adj := _}
source
@[simp]
theorem simple_graph.dart.edge_symm {V : Type u} {G : simple_graph V} (d : G.dart) :
d.symm.edge = d.edge
source
@[simp]
theorem simple_graph.dart.edge_comp_symm {V : Type u} {G : simple_graph V} :
simple_graph.dart.edge ∘ simple_graph.dart.symm = simple_graph.dart.edge
source
@[simp]
theorem simple_graph.dart.symm_symm {V : Type u} {G : simple_graph V} (d : G.dart) :
d.symm.symm = d
source
@[simp]
theorem simple_graph.dart.symm_involutive {V : Type u} {G : simple_graph V} :
function.involutive simple_graph.dart.symm
source
theorem simple_graph.dart.symm_ne {V : Type u} {G : simple_graph V} (d : G.dart) :
d.symm ≠ d
source
theorem simple_graph.dart_edge_eq_iff {V : Type u} {G : simple_graph V} (d₁ d₂ : G.dart) :
d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.symm
source
theorem simple_graph.dart_edge_eq_mk_iff {V : Type u} {G : simple_graph V} {d : G.dart} {p : V × V} :
d.edge = ⟦p⟧ ↔ d.to_prod = p ∨ d.to_prod = p.swap
source
theorem simple_graph.dart_edge_eq_mk_iff' {V : Type u} {G : simple_graph V} {d : G.dart} {u v : V} :
d.edge = ⟦(u, v)⟧ ↔ d.to_prod.fst = u ∧ d.to_prod.snd = v ∨ d.to_prod.fst = v ∧ d.to_prod.snd = u
source
def simple_graph.dart_adj {V : Type u} (G : simple_graph V) (d d' : G.dart) :
Prop

Two darts are said to be adjacent if they could be consecutive darts in a walk -- that is, the first dart's second vertex is equal to the second dart's first vertex.

Equations
source
def simple_graph.dart_of_neighbor_set {V : Type u} (G : simple_graph V) (v : V) (w : ↥(G.neighbor_set v)) :
G.dart

For a given vertex v, this is the bijective map from the neighbor set at v to the darts d with d.fst = v.

Equations
source
@[simp]
theorem simple_graph.dart_of_neighbor_set_to_prod {V : Type u} (G : simple_graph V) (v : V) (w : ↥(G.neighbor_set v)) :
(G.dart_of_neighbor_set v w).to_prod = (v, ↑w)
source
theorem simple_graph.dart_of_neighbor_set_injective {V : Type u} (G : simple_graph V) (v : V) :
function.injective (G.dart_of_neighbor_set v)
source
@[protected, instance]
def simple_graph.nonempty_dart_top {V : Type u} [nontrivial V] :
nonempty ⊤.dart

Incidence set #

source
def simple_graph.incidence_set {V : Type u} (G : simple_graph V) (v : V) :
set (sym2 V)

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

Equations
Instances for ↥simple_graph.incidence_set
source
theorem simple_graph.incidence_set_subset {V : Type u} (G : simple_graph V) (v : V) :
G.incidence_set v ⊆ ⇑simple_graph.edge_set G
source
theorem simple_graph.mk_mem_incidence_set_iff {V : Type u} (G : simple_graph V) {a b c : V} :
⟦(b, c)⟧ ∈ G.incidence_set a ↔ G.adj b c ∧ (a = b ∨ a = c)
source
theorem simple_graph.mk_mem_incidence_set_left_iff {V : Type u} (G : simple_graph V) {a b : V} :
⟦(a, b)⟧ ∈ G.incidence_set a ↔ G.adj a b
source
theorem simple_graph.mk_mem_incidence_set_right_iff {V : Type u} (G : simple_graph V) {a b : V} :
⟦(a, b)⟧ ∈ G.incidence_set b ↔ G.adj a b
source
theorem simple_graph.edge_mem_incidence_set_iff {V : Type u} (G : simple_graph V) {a : V} {e : ↥(⇑simple_graph.edge_set G)} :
↑e ∈ G.incidence_set a ↔ a ∈ ↑e
source
theorem simple_graph.incidence_set_inter_incidence_set_subset {V : Type u} (G : simple_graph V) {a b : V} (h : a ≠ b) :
G.incidence_set a ∩ G.incidence_set b ⊆ {⟦(a, b)⟧}
source
theorem simple_graph.incidence_set_inter_incidence_set_of_adj {V : Type u} (G : simple_graph V) {a b : V} (h : G.adj a b) :
G.incidence_set a ∩ G.incidence_set b = {⟦(a, b)⟧}
source
theorem simple_graph.adj_of_mem_incidence_set {V : Type u} (G : simple_graph V) {a b : V} {e : sym2 V} (h : a ≠ b) (ha : e ∈ G.incidence_set a) (hb : e ∈ G.incidence_set b) :
G.adj a b
source
theorem simple_graph.incidence_set_inter_incidence_set_of_not_adj {V : Type u} (G : simple_graph V) {a b : V} (h : ¬G.adj a b) (hn : a ≠ b) :
G.incidence_set a ∩ G.incidence_set b = ∅
source
@[protected, instance]
def simple_graph.decidable_mem_incidence_set {V : Type u} (G : simple_graph V) [decidable_eq V] [decidable_rel G.adj] (v : V) :
decidable_pred (λ (_x : sym2 V), _x ∈ G.incidence_set v)
Equations
source
@[reducible]
def simple_graph.edge_finset {V : Type u} (G : simple_graph V) [fintype ↥(⇑simple_graph.edge_set G)] :
finset (sym2 V)

The edge_set of the graph as a finset.

Equations
source
@[simp, norm_cast]
theorem simple_graph.coe_edge_finset {V : Type u} (G : simple_graph V) [fintype ↥(⇑simple_graph.edge_set G)] :
↑(G.edge_finset) = ⇑simple_graph.edge_set G
source
@[simp]
theorem simple_graph.mem_edge_finset {V : Type u} {G : simple_graph V} {e : sym2 V} [fintype ↥(⇑simple_graph.edge_set G)] :
e ∈ G.edge_finset ↔ e ∈ ⇑simple_graph.edge_set G
source
theorem simple_graph.not_is_diag_of_mem_edge_finset {V : Type u} {G : simple_graph V} {e : sym2 V} [fintype ↥(⇑simple_graph.edge_set G)] :
e ∈ G.edge_finset → ¬e.is_diag
source
@[simp]
theorem simple_graph.edge_finset_inj {V : Type u} {G₁ G₂ : simple_graph V} [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] :
G₁.edge_finset = G₂.edge_finset ↔ G₁ = G₂
source
@[simp]
theorem simple_graph.edge_finset_subset_edge_finset {V : Type u} {G₁ G₂ : simple_graph V} [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] :
G₁.edge_finset ⊆ G₂.edge_finset ↔ G₁ ≤ G₂
source
@[simp]
theorem simple_graph.edge_finset_ssubset_edge_finset {V : Type u} {G₁ G₂ : simple_graph V} [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] :
G₁.edge_finset ⊂ G₂.edge_finset ↔ G₁ < G₂
source
theorem simple_graph.edge_finset_mono {V : Type u} {G₁ G₂ : simple_graph V} [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] :
G₁ ≤ G₂ → G₁.edge_finset ⊆ G₂.edge_finset

Alias of the reverse direction of simple_graph.edge_finset_subset_edge_finset.

source
theorem simple_graph.edge_finset_strict_mono {V : Type u} {G₁ G₂ : simple_graph V} [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] :
G₁ < G₂ → G₁.edge_finset ⊂ G₂.edge_finset

Alias of the reverse direction of simple_graph.edge_finset_ssubset_edge_finset.

source
@[simp]
theorem simple_graph.edge_finset_bot {V : Type u} :
⊥.edge_finset = ∅
source
@[simp]
theorem simple_graph.edge_finset_sup {V : Type u} {G₁ G₂ : simple_graph V} [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] [decidable_eq V] :
(G₁ ⊔ G₂).edge_finset = G₁.edge_finset ∪ G₂.edge_finset
source
@[simp]
theorem simple_graph.edge_finset_inf {V : Type u} {G₁ G₂ : simple_graph V} [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] [decidable_eq V] :
(G₁ ⊓ G₂).edge_finset = G₁.edge_finset ∩ G₂.edge_finset
source
@[simp]
theorem simple_graph.edge_finset_sdiff {V : Type u} {G₁ G₂ : simple_graph V} [fintype ↥(⇑simple_graph.edge_set G₁)] [fintype ↥(⇑simple_graph.edge_set G₂)] [decidable_eq V] :
(G₁ \ G₂).edge_finset = G₁.edge_finset \ G₂.edge_finset
source
theorem simple_graph.edge_finset_card {V : Type u} {G : simple_graph V} [fintype ↥(⇑simple_graph.edge_set G)] :
G.edge_finset.card = fintype.card ↥(⇑simple_graph.edge_set G)
source
@[simp]
theorem simple_graph.edge_set_univ_card {V : Type u} {G : simple_graph V} [fintype ↥(⇑simple_graph.edge_set G)] :
finset.univ.card = G.edge_finset.card
source
@[simp]
theorem simple_graph.mem_neighbor_set {V : Type u} (G : simple_graph V) (v w : V) :
w ∈ G.neighbor_set v ↔ G.adj v w
source
@[simp]
theorem simple_graph.mem_incidence_set {V : Type u} (G : simple_graph V) (v w : V) :
⟦(v, w)⟧ ∈ G.incidence_set v ↔ G.adj v w
source
theorem simple_graph.mem_incidence_iff_neighbor {V : Type u} (G : simple_graph V) {v w : V} :
⟦(v, w)⟧ ∈ G.incidence_set v ↔ w ∈ G.neighbor_set v
source
theorem simple_graph.adj_incidence_set_inter {V : Type u} (G : simple_graph V) {v : V} {e : sym2 V} (he : e ∈ ⇑simple_graph.edge_set G) (h : v ∈ e) :
G.incidence_set v ∩ G.incidence_set (sym2.mem.other h) = {e}
source
theorem simple_graph.compl_neighbor_set_disjoint {V : Type u} (G : simple_graph V) (v : V) :
disjoint (G.neighbor_set v) (Gᶜ.neighbor_set v)
source
theorem simple_graph.neighbor_set_union_compl_neighbor_set_eq {V : Type u} (G : simple_graph V) (v : V) :
G.neighbor_set v ∪ Gᶜ.neighbor_set v = {v}ᶜ
source
theorem simple_graph.card_neighbor_set_union_compl_neighbor_set {V : Type u} [fintype V] (G : simple_graph V) (v : V) [h : fintype ↥(G.neighbor_set v ∪ Gᶜ.neighbor_set v)] :
(G.neighbor_set v ∪ Gᶜ.neighbor_set v).to_finset.card = fintype.card V - 1
source
theorem simple_graph.neighbor_set_compl {V : Type u} (G : simple_graph V) (v : V) :
Gᶜ.neighbor_set v = (G.neighbor_set v)ᶜ \ {v}
source
def simple_graph.common_neighbors {V : Type u} (G : simple_graph 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
source
theorem simple_graph.common_neighbors_eq {V : Type u} (G : simple_graph V) (v w : V) :
G.common_neighbors v w = G.neighbor_set v ∩ G.neighbor_set w
source
theorem simple_graph.mem_common_neighbors {V : Type u} (G : simple_graph V) {u v w : V} :
u ∈ G.common_neighbors v w ↔ G.adj v u ∧ G.adj w u
source
theorem simple_graph.common_neighbors_symm {V : Type u} (G : simple_graph V) (v w : V) :
G.common_neighbors v w = G.common_neighbors w v
source
theorem simple_graph.not_mem_common_neighbors_left {V : Type u} (G : simple_graph V) (v w : V) :
v ∉ G.common_neighbors v w
source
theorem simple_graph.not_mem_common_neighbors_right {V : Type u} (G : simple_graph V) (v w : V) :
w ∉ G.common_neighbors v w
source
theorem simple_graph.common_neighbors_subset_neighbor_set_left {V : Type u} (G : simple_graph V) (v w : V) :
G.common_neighbors v w ⊆ G.neighbor_set v
source
theorem simple_graph.common_neighbors_subset_neighbor_set_right {V : Type u} (G : simple_graph V) (v w : V) :
G.common_neighbors v w ⊆ G.neighbor_set w
source
@[protected, instance]
def simple_graph.decidable_mem_common_neighbors {V : Type u} (G : simple_graph V) [decidable_rel G.adj] (v w : V) :
decidable_pred (λ (_x : V), _x ∈ G.common_neighbors v w)
Equations
source
theorem simple_graph.common_neighbors_top_eq {V : Type u} {v w : V} :
⊤.common_neighbors v w = set.univ \ {v, w}
source
def simple_graph.other_vertex_of_incident {V : Type u} (G : simple_graph V) [decidable_eq V] {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) :
V

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

Equations
source
theorem simple_graph.edge_other_incident_set {V : Type u} (G : simple_graph V) [decidable_eq V] {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) :
e ∈ G.incidence_set (G.other_vertex_of_incident h)
source
theorem simple_graph.incidence_other_prop {V : Type u} (G : simple_graph V) [decidable_eq V] {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) :
G.other_vertex_of_incident h ∈ G.neighbor_set v
source
@[simp]
theorem simple_graph.incidence_other_neighbor_edge {V : Type u} (G : simple_graph V) [decidable_eq V] {v w : V} (h : w ∈ G.neighbor_set v) :
G.other_vertex_of_incident _ = w
source
@[simp]
theorem simple_graph.incidence_set_equiv_neighbor_set_apply_coe {V : Type u} (G : simple_graph V) [decidable_eq V] (v : V) (e : ↥(G.incidence_set v)) :
↑(⇑(G.incidence_set_equiv_neighbor_set v) e) = G.other_vertex_of_incident _
source
@[simp]
theorem simple_graph.incidence_set_equiv_neighbor_set_symm_apply_coe {V : Type u} (G : simple_graph V) [decidable_eq V] (v : V) (w : ↥(G.neighbor_set v)) :
↑(⇑((G.incidence_set_equiv_neighbor_set v).symm) w) = ⟦(v, w.val)⟧
source
def simple_graph.incidence_set_equiv_neighbor_set {V : Type u} (G : simple_graph V) [decidable_eq V] (v : V) :
↥(G.incidence_set v) ≃ ↥(G.neighbor_set 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

Edge deletion #

source
def simple_graph.delete_edges {V : Type u} (G : simple_graph V) (s : set (sym2 V)) :
simple_graph V

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

See also: simple_graph.subgraph.delete_edges.

Equations
source
@[simp]
theorem simple_graph.delete_edges_adj {V : Type u} (G : simple_graph V) (s : set (sym2 V)) (v w : V) :
(G.delete_edges s).adj v w ↔ G.adj v w ∧ ⟦(v, w)⟧ ∉ s
source
theorem simple_graph.sdiff_eq_delete_edges {V : Type u} (G G' : simple_graph V) :
G \ G' = G.delete_edges (⇑simple_graph.edge_set G')
source
theorem simple_graph.delete_edges_eq_sdiff_from_edge_set {V : Type u} (G : simple_graph V) (s : set (sym2 V)) :
G.delete_edges s = G \ simple_graph.from_edge_set s
source
theorem simple_graph.compl_eq_delete_edges {V : Type u} (G : simple_graph V) :
Gᶜ = ⊤.delete_edges (⇑simple_graph.edge_set G)
source
@[simp]
theorem simple_graph.delete_edges_delete_edges {V : Type u} (G : simple_graph V) (s s' : set (sym2 V)) :
(G.delete_edges s).delete_edges s' = G.delete_edges (s ∪ s')
source
@[simp]
theorem simple_graph.delete_edges_empty_eq {V : Type u} (G : simple_graph V) :
G.delete_edges ∅ = G
source
@[simp]
theorem simple_graph.delete_edges_univ_eq {V : Type u} (G : simple_graph V) :
G.delete_edges set.univ = ⊥
source
theorem simple_graph.delete_edges_le {V : Type u} (G : simple_graph V) (s : set (sym2 V)) :
G.delete_edges s ≤ G
source
theorem simple_graph.delete_edges_le_of_le {V : Type u} (G : simple_graph V) {s s' : set (sym2 V)} (h : s ⊆ s') :
G.delete_edges s' ≤ G.delete_edges s
source
theorem simple_graph.delete_edges_eq_inter_edge_set {V : Type u} (G : simple_graph V) (s : set (sym2 V)) :
G.delete_edges s = G.delete_edges (s ∩ ⇑simple_graph.edge_set G)
source
theorem simple_graph.delete_edges_sdiff_eq_of_le {V : Type u} (G : simple_graph V) {H : simple_graph V} (h : H ≤ G) :
G.delete_edges (⇑simple_graph.edge_set G \ ⇑simple_graph.edge_set H) = H
source
theorem simple_graph.edge_set_delete_edges {V : Type u} (G : simple_graph V) (s : set (sym2 V)) :
⇑simple_graph.edge_set (G.delete_edges s) = ⇑simple_graph.edge_set G \ s
source
theorem simple_graph.edge_finset_delete_edges {V : Type u} (G : simple_graph V) [fintype V] [decidable_eq V] [decidable_rel G.adj] (s : finset (sym2 V)) [decidable_rel (G.delete_edges ↑s).adj] :
(G.delete_edges ↑s).edge_finset = G.edge_finset \ s
source
def simple_graph.delete_far {𝕜 : Type u_1} {V : Type u} (G : simple_graph V) [ordered_ring 𝕜] [fintype V] [decidable_eq V] [decidable_rel G.adj] (p : simple_graph V → Prop) (r : 𝕜) :
Prop

A graph is r-delete-far from a property p if we must delete at least r edges from it to get a graph with the property p.

Equations
source
theorem simple_graph.delete_far_iff {𝕜 : Type u_1} {V : Type u} {G : simple_graph V} [ordered_ring 𝕜] [fintype V] [decidable_eq V] [decidable_rel G.adj] {p : simple_graph V → Prop} {r : 𝕜} :
G.delete_far p r ↔ ∀ ⦃H : simple_graph V⦄, H ≤ G → p H → r ≤ ↑(G.edge_finset.card) - ↑(H.edge_finset.card)
source
theorem simple_graph.delete_far.le_card_sub_card {𝕜 : Type u_1} {V : Type u} {G : simple_graph V} [ordered_ring 𝕜] [fintype V] [decidable_eq V] [decidable_rel G.adj] {p : simple_graph V → Prop} {r : 𝕜} :
G.delete_far p r → ∀ ⦃H : simple_graph V⦄, H ≤ G → p H → r ≤ ↑(G.edge_finset.card) - ↑(H.edge_finset.card)

Alias of the forward direction of simple_graph.delete_far_iff.

source
theorem simple_graph.delete_far.mono {𝕜 : Type u_1} {V : Type u} {G : simple_graph V} [ordered_ring 𝕜] [fintype V] [decidable_eq V] [decidable_rel G.adj] {p : simple_graph V → Prop} {r₁ r₂ : 𝕜} (h : G.delete_far p r₂) (hr : r₁ ≤ r₂) :
G.delete_far p r₁

Map and comap #

source
@[protected]
def simple_graph.map {V : Type u} {W : Type v} (f : V ↪ W) (G : simple_graph V) :
simple_graph W

Given an injective function, there is an covariant induced map on graphs by pushing forward the adjacency relation.

This is injective (see simple_graph.map_injective).

Equations
source
@[simp]
theorem simple_graph.map_adj {V : Type u} {W : Type v} (f : V ↪ W) (G : simple_graph V) (u v : W) :
(simple_graph.map f G).adj u v ↔ ∃ (u' v' : V), G.adj u' v' ∧ ⇑f u' = u ∧ ⇑f v' = v
source
theorem simple_graph.map_monotone {V : Type u} {W : Type v} (f : V ↪ W) :
monotone (simple_graph.map f)
source
@[simp]
theorem simple_graph.comap_adj {V : Type u} {W : Type v} (f : V → W) (G : simple_graph W) (u v : V) :
(simple_graph.comap f G).adj u v = G.adj (f u) (f v)
source
@[protected]
def simple_graph.comap {V : Type u} {W : Type v} (f : V → W) (G : simple_graph W) :
simple_graph V

Given a function, there is a contravariant induced map on graphs by pulling back the adjacency relation. This is one of the ways of creating induced graphs. See simple_graph.induce for a wrapper.

This is surjective when f is injective (see simple_graph.comap_surjective).

Equations
source
theorem simple_graph.comap_monotone {V : Type u} {W : Type v} (f : V ↪ W) :
monotone (simple_graph.comap ⇑f)
source
@[simp]
theorem simple_graph.comap_map_eq {V : Type u} {W : Type v} (f : V ↪ W) (G : simple_graph V) :
simple_graph.comap ⇑f (simple_graph.map f G) = G
source
theorem simple_graph.left_inverse_comap_map {V : Type u} {W : Type v} (f : V ↪ W) :
function.left_inverse (simple_graph.comap ⇑f) (simple_graph.map f)
source
theorem simple_graph.map_injective {V : Type u} {W : Type v} (f : V ↪ W) :
function.injective (simple_graph.map f)
source
theorem simple_graph.comap_surjective {V : Type u} {W : Type v} (f : V ↪ W) :
function.surjective (simple_graph.comap ⇑f)
source
theorem simple_graph.map_le_iff_le_comap {V : Type u} {W : Type v} (f : V ↪ W) (G : simple_graph V) (G' : simple_graph W) :
simple_graph.map f G ≤ G' ↔ G ≤ simple_graph.comap ⇑f G'
source
theorem simple_graph.map_comap_le {V : Type u} {W : Type v} (f : V ↪ W) (G : simple_graph W) :
simple_graph.map f (simple_graph.comap ⇑f G) ≤ G

Induced graphs #

source
@[reducible]
def simple_graph.induce {V : Type u} (s : set V) (G : simple_graph V) :
simple_graph ↥s

Restrict a graph to the vertices in the set s, deleting all edges incident to vertices outside the set. This is a wrapper around simple_graph.comap.

Equations
source
@[reducible]
def simple_graph.spanning_coe {V : Type u} {s : set V} (G : simple_graph ↥s) :
simple_graph V

Given a graph on a set of vertices, we can make it be a simple_graph V by adding in the remaining vertices without adding in any additional edges. This is a wrapper around simple_graph.map.

Equations
source
theorem simple_graph.induce_spanning_coe {V : Type u} {s : set V} {G : simple_graph ↥s} :
simple_graph.induce s G.spanning_coe = G
source
theorem simple_graph.spanning_coe_induce_le {V : Type u} (G : simple_graph V) (s : set V) :
(simple_graph.induce s G).spanning_coe ≤ G

Finiteness at a vertex #

This section contains definitions and lemmas concerning vertices that have finitely many adjacent vertices. We denote this condition by fintype (G.neighbor_set v).

We define G.neighbor_finset v to be the finset version of G.neighbor_set v. Use neighbor_finset_eq_filter to rewrite this definition as a filter.

source
def simple_graph.neighbor_finset {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :
finset V

G.neighbors v is the finset version of G.adj v in case G is locally finite at v.

Equations
source
theorem simple_graph.neighbor_finset_def {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :
G.neighbor_finset v = (G.neighbor_set v).to_finset
source
@[simp]
theorem simple_graph.mem_neighbor_finset {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] (w : V) :
w ∈ G.neighbor_finset v ↔ G.adj v w
source
@[simp]
theorem simple_graph.not_mem_neighbor_finset_self {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :
v ∉ G.neighbor_finset v
source
theorem simple_graph.neighbor_finset_disjoint_singleton {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :
disjoint (G.neighbor_finset v) {v}
source
theorem simple_graph.singleton_disjoint_neighbor_finset {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :
disjoint {v} (G.neighbor_finset v)
source
def simple_graph.degree {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :
ℕ

G.degree v is the number of vertices adjacent to v.

Equations
source
@[simp]
theorem simple_graph.card_neighbor_set_eq_degree {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :
fintype.card ↥(G.neighbor_set v) = G.degree v
source
theorem simple_graph.degree_pos_iff_exists_adj {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :
0 < G.degree v ↔ ∃ (w : V), G.adj v w
source
theorem simple_graph.degree_compl {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] [fintype ↥(Gᶜ.neighbor_set v)] [fintype V] :
Gᶜ.degree v = fintype.card V - 1 - G.degree v
source
@[protected, instance]
def simple_graph.incidence_set_fintype {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] [decidable_eq V] :
fintype ↥(G.incidence_set v)
Equations
source
def simple_graph.incidence_finset {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] [decidable_eq V] :
finset (sym2 V)

This is the finset version of incidence_set.

Equations
source
@[simp]
theorem simple_graph.card_incidence_set_eq_degree {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] [decidable_eq V] :
fintype.card ↥(G.incidence_set v) = G.degree v
source
@[simp]
theorem simple_graph.card_incidence_finset_eq_degree {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] [decidable_eq V] :
(G.incidence_finset v).card = G.degree v
source
@[simp]
theorem simple_graph.mem_incidence_finset {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] [decidable_eq V] (e : sym2 V) :
e ∈ G.incidence_finset v ↔ e ∈ G.incidence_set v
source
theorem simple_graph.incidence_finset_eq_filter {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] [decidable_eq V] [fintype ↥(⇑simple_graph.edge_set G)] :
G.incidence_finset v = finset.filter (has_mem.mem v) G.edge_finset
source
@[reducible]
def simple_graph.locally_finite {V : Type u} (G : simple_graph V) :
Type u

A graph is locally finite if every vertex has a finite neighbor set.

Equations
source
def simple_graph.is_regular_of_degree {V : Type u} (G : simple_graph V) [G.locally_finite] (d : ℕ) :
Prop

A locally finite simple graph is regular of degree d if every vertex has degree d.

Equations
source
theorem simple_graph.is_regular_of_degree.degree_eq {V : Type u} {G : simple_graph V} [G.locally_finite] {d : ℕ} (h : G.is_regular_of_degree d) (v : V) :
G.degree v = d
source
theorem simple_graph.is_regular_of_degree.compl {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {k : ℕ} (h : G.is_regular_of_degree k) :
Gᶜ.is_regular_of_degree (fintype.card V - 1 - k)
source
@[protected, instance]
def simple_graph.neighbor_set_fintype {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v : V) :
fintype ↥(G.neighbor_set v)
Equations
source
theorem simple_graph.neighbor_finset_eq_filter {V : Type u} (G : simple_graph V) [fintype V] {v : V} [decidable_rel G.adj] :
G.neighbor_finset v = finset.filter (G.adj v) finset.univ
source
theorem simple_graph.neighbor_finset_compl {V : Type u} (G : simple_graph V) [fintype V] [decidable_eq V] [decidable_rel G.adj] (v : V) :
Gᶜ.neighbor_finset v = (G.neighbor_finset v)ᶜ \ {v}
source
@[simp]
theorem simple_graph.complete_graph_degree {V : Type u} [fintype V] [decidable_eq V] (v : V) :
⊤.degree v = fintype.card V - 1
source
theorem simple_graph.bot_degree {V : Type u} [fintype V] (v : V) :
⊥.degree v = 0
source
theorem simple_graph.is_regular_of_degree.top {V : Type u} [fintype V] [decidable_eq V] :
⊤.is_regular_of_degree (fintype.card V - 1)
source
def simple_graph.min_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] :
ℕ

The minimum degree of all vertices (and 0 if there are no vertices). The key properties of this are given in exists_minimal_degree_vertex, min_degree_le_degree and le_min_degree_of_forall_le_degree.

Equations
source
theorem simple_graph.exists_minimal_degree_vertex {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [nonempty V] :
∃ (v : V), G.min_degree = G.degree v

There exists a vertex of minimal degree. Note the assumption of being nonempty is necessary, as the lemma implies there exists a vertex.

source
theorem simple_graph.min_degree_le_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v : V) :
G.min_degree ≤ G.degree v

The minimum degree in the graph is at most the degree of any particular vertex.

source
theorem simple_graph.le_min_degree_of_forall_le_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [nonempty V] (k : ℕ) (h : ∀ (v : V), k ≤ G.degree v) :
k ≤ G.min_degree

In a nonempty graph, if k is at most the degree of every vertex, it is at most the minimum degree. Note the assumption that the graph is nonempty is necessary as long as G.min_degree is defined to be a natural.

source
def simple_graph.max_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] :
ℕ

The maximum degree of all vertices (and 0 if there are no vertices). The key properties of this are given in exists_maximal_degree_vertex, degree_le_max_degree and max_degree_le_of_forall_degree_le.

Equations
source
theorem simple_graph.exists_maximal_degree_vertex {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [nonempty V] :
∃ (v : V), G.max_degree = G.degree v

There exists a vertex of maximal degree. Note the assumption of being nonempty is necessary, as the lemma implies there exists a vertex.

source
theorem simple_graph.degree_le_max_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v : V) :
G.degree v ≤ G.max_degree

The maximum degree in the graph is at least the degree of any particular vertex.

source
theorem simple_graph.max_degree_le_of_forall_degree_le {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (k : ℕ) (h : ∀ (v : V), G.degree v ≤ k) :
G.max_degree ≤ k

In a graph, if k is at least the degree of every vertex, then it is at least the maximum degree.

source
theorem simple_graph.degree_lt_card_verts {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v : V) :
G.degree v < fintype.card V
source
theorem simple_graph.max_degree_lt_card_verts {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [nonempty V] :
G.max_degree < fintype.card V

The maximum degree of a nonempty graph is less than the number of vertices. Note that the assumption that V is nonempty is necessary, as otherwise this would assert the existence of a natural number less than zero.

source
theorem simple_graph.card_common_neighbors_le_degree_left {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v w : V) :
fintype.card ↥(G.common_neighbors v w) ≤ G.degree v
source
theorem simple_graph.card_common_neighbors_le_degree_right {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v w : V) :
fintype.card ↥(G.common_neighbors v w) ≤ G.degree w
source
theorem simple_graph.card_common_neighbors_lt_card_verts {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v w : V) :
fintype.card ↥(G.common_neighbors v w) < fintype.card V
source
theorem simple_graph.adj.card_common_neighbors_lt_degree {V : Type u} [fintype V] {G : simple_graph V} [decidable_rel G.adj] {v w : V} (h : G.adj v w) :
fintype.card ↥(G.common_neighbors v w) < G.degree v

If the condition G.adj v w fails, then card_common_neighbors_le_degree is the best we can do in general.

source
theorem simple_graph.card_common_neighbors_top {V : Type u} [fintype V] [decidable_eq V] {v w : V} (h : v ≠ w) :
fintype.card ↥(⊤.common_neighbors v w) = fintype.card V - 2
source
@[reducible]
def simple_graph.hom {V : Type u} {W : Type v} (G : simple_graph V) (G' : simple_graph W) :
Type (max u v)

A graph homomorphism is a map on vertex sets that respects adjacency relations.

The notation G →g G' represents the type of graph homomorphisms.

source
@[reducible]
def simple_graph.embedding {V : Type u} {W : Type v} (G : simple_graph V) (G' : simple_graph W) :
Type (max u v)

A graph embedding is an embedding f such that for vertices v w : V, G.adj f(v) f(w) ↔ G.adj v w. Its image is an induced subgraph of G'.

The notation G ↪g G' represents the type of graph embeddings.

source
@[reducible]
def simple_graph.iso {V : Type u} {W : Type v} (G : simple_graph V) (G' : simple_graph W) :
Type (max u v)

A graph isomorphism is an bijective map on vertex sets that respects adjacency relations.

The notation G ≃g G' represents the type of graph isomorphisms.

source
@[reducible]
def simple_graph.hom.id {V : Type u} {G : simple_graph V} :
G →g G

The identity homomorphism from a graph to itself.

source
theorem simple_graph.hom.map_adj {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') {v w : V} (h : G.adj v w) :
G'.adj (⇑f v) (⇑f w)
source
theorem simple_graph.hom.map_mem_edge_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') {e : sym2 V} (h : e ∈ ⇑simple_graph.edge_set G) :
sym2.map ⇑f e ∈ ⇑simple_graph.edge_set G'
source
theorem simple_graph.hom.apply_mem_neighbor_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') {v w : V} (h : w ∈ G.neighbor_set v) :
⇑f w ∈ G'.neighbor_set (⇑f v)
source
def simple_graph.hom.map_edge_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (e : ↥(⇑simple_graph.edge_set G)) :
↥(⇑simple_graph.edge_set G')

The map between edge sets induced by a homomorphism. The underlying map on edges is given by sym2.map.

Equations
source
@[simp]
theorem simple_graph.hom.map_edge_set_coe {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (e : ↥(⇑simple_graph.edge_set G)) :
↑(f.map_edge_set e) = sym2.map ⇑f ↑e
source
@[simp]
theorem simple_graph.hom.map_neighbor_set_coe {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (v : V) (w : ↥(G.neighbor_set v)) :
↑(f.map_neighbor_set v w) = ⇑f ↑w
source
def simple_graph.hom.map_neighbor_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (v : V) (w : ↥(G.neighbor_set v)) :
↥(G'.neighbor_set (⇑f v))

The map between neighbor sets induced by a homomorphism.

Equations
source
def simple_graph.hom.map_dart {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (d : G.dart) :
G'.dart

The map between darts induced by a homomorphism.

Equations
source
@[simp]
theorem simple_graph.hom.map_dart_apply {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (d : G.dart) :
f.map_dart d = {to_prod := prod.map ⇑f ⇑f d.to_prod, is_adj := _}
source
def simple_graph.hom.map_spanning_subgraphs {V : Type u} {G G' : simple_graph V} (h : G ≤ G') :
G →g G'

The induced map for spanning subgraphs, which is the identity on vertices.

Equations
source
@[simp]
theorem simple_graph.hom.map_spanning_subgraphs_apply {V : Type u} {G G' : simple_graph V} (h : G ≤ G') (x : V) :
⇑(simple_graph.hom.map_spanning_subgraphs h) x = x
source
theorem simple_graph.hom.map_edge_set.injective {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (hinj : function.injective ⇑f) :
function.injective f.map_edge_set
source
theorem simple_graph.hom.injective_of_top_hom {V : Type u} {W : Type v} {G' : simple_graph W} (f : ⊤ →g G') :
function.injective ⇑f

Every graph homomomorphism from a complete graph is injective.

source
@[simp]
theorem simple_graph.hom.comap_apply {V : Type u} {W : Type v} (f : V → W) (G : simple_graph W) (ᾰ : V) :
⇑(simple_graph.hom.comap f G) ᾰ = f ᾰ
source
@[protected]
def simple_graph.hom.comap {V : Type u} {W : Type v} (f : V → W) (G : simple_graph W) :
simple_graph.comap f G →g G

There is a homomorphism to a graph from a comapped graph. When the function is injective, this is an embedding (see simple_graph.embedding.comap).

Equations
source
@[reducible]
def simple_graph.hom.comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' →g G'') (f : G →g G') :
G →g G''

Composition of graph homomorphisms.

source
@[simp]
theorem simple_graph.hom.coe_comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' →g G'') (f : G →g G') :
⇑(f'.comp f) = ⇑f' ∘ ⇑f
source
@[reducible]
def simple_graph.embedding.refl {V : Type u} {G : simple_graph V} :
G ↪g G

The identity embedding from a graph to itself.

source
@[reducible]
def simple_graph.embedding.to_hom {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') :
G →g G'

An embedding of graphs gives rise to a homomorphism of graphs.

source
theorem simple_graph.embedding.map_adj_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') {v w : V} :
G'.adj (⇑f v) (⇑f w) ↔ G.adj v w
source
theorem simple_graph.embedding.map_mem_edge_set_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') {e : sym2 V} :
sym2.map ⇑f e ∈ ⇑simple_graph.edge_set G' ↔ e ∈ ⇑simple_graph.edge_set G
source
theorem simple_graph.embedding.apply_mem_neighbor_set_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') {v w : V} :
⇑f w ∈ G'.neighbor_set (⇑f v) ↔ w ∈ G.neighbor_set v
source
@[simp]
theorem simple_graph.embedding.map_edge_set_apply {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') (e : ↥(⇑simple_graph.edge_set G)) :
⇑(f.map_edge_set) e = ↑f.map_edge_set e
source
def simple_graph.embedding.map_edge_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') :
↥(⇑simple_graph.edge_set G) ↪ ↥(⇑simple_graph.edge_set G')

A graph embedding induces an embedding of edge sets.

Equations
source
def simple_graph.embedding.map_neighbor_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') (v : V) :
↥(G.neighbor_set v) ↪ ↥(G'.neighbor_set (⇑f v))

A graph embedding induces an embedding of neighbor sets.

Equations
source
@[simp]
theorem simple_graph.embedding.map_neighbor_set_apply_coe {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') (v : V) (w : ↥(G.neighbor_set v)) :
↑(⇑(f.map_neighbor_set v) w) = ⇑f ↑w
source
@[protected]
def simple_graph.embedding.comap {V : Type u} {W : Type v} (f : V ↪ W) (G : simple_graph W) :
simple_graph.comap ⇑f G ↪g G

Given an injective function, there is an embedding from the comapped graph into the original graph.

Equations
source
@[simp]
theorem simple_graph.embedding.comap_apply {V : Type u} {W : Type v} (f : V ↪ W) (G : simple_graph W) (ᾰ : V) :
⇑(simple_graph.embedding.comap f G) ᾰ = f.to_fun ᾰ
source
@[protected]
def simple_graph.embedding.map {V : Type u} {W : Type v} (f : V ↪ W) (G : simple_graph V) :
G ↪g simple_graph.map f G

Given an injective function, there is an embedding from a graph into the mapped graph.

Equations
source
@[simp]
theorem simple_graph.embedding.map_apply {V : Type u} {W : Type v} (f : V ↪ W) (G : simple_graph V) (ᾰ : V) :
⇑(simple_graph.embedding.map f G) ᾰ = f.to_fun ᾰ
source
@[protected, reducible]
def simple_graph.embedding.induce {V : Type u} {G : simple_graph V} (s : set V) :
simple_graph.induce s G ↪g G

Induced graphs embed in the original graph.

Note that if G.induce s = ⊤ (i.e., if s is a clique) then this gives the embedding of a complete graph.

Equations
source
@[protected, reducible]
def simple_graph.embedding.spanning_coe {V : Type u} {s : set V} (G : simple_graph ↥s) :
G ↪g G.spanning_coe

Graphs on a set of vertices embed in their spanning_coe.

Equations
source
@[protected]
def simple_graph.embedding.complete_graph {α : Type u_1} {β : Type u_2} (f : α ↪ β) :
⊤ ↪g ⊤

Embeddings of types induce embeddings of complete graphs on those types.

Equations
source
@[reducible]
def simple_graph.embedding.comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' ↪g G'') (f : G ↪g G') :
G ↪g G''

Composition of graph embeddings.

source
@[simp]
theorem simple_graph.embedding.coe_comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' ↪g G'') (f : G ↪g G') :
⇑(f'.comp f) = ⇑f' ∘ ⇑f
source
@[reducible]
def simple_graph.iso.refl {V : Type u} {G : simple_graph V} :
G ≃g G

The identity isomorphism of a graph with itself.

source
@[reducible]
def simple_graph.iso.to_embedding {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') :
G ↪g G'

An isomorphism of graphs gives rise to an embedding of graphs.

source
@[reducible]
def simple_graph.iso.to_hom {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') :
G →g G'

An isomorphism of graphs gives rise to a homomorphism of graphs.

source
@[reducible]
def simple_graph.iso.symm {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') :
G' ≃g G

The inverse of a graph isomorphism.

source
theorem simple_graph.iso.map_adj_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') {v w : V} :
G'.adj (⇑f v) (⇑f w) ↔ G.adj v w
source
theorem simple_graph.iso.map_mem_edge_set_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') {e : sym2 V} :
sym2.map ⇑f e ∈ ⇑simple_graph.edge_set G' ↔ e ∈ ⇑simple_graph.edge_set G
source
theorem simple_graph.iso.apply_mem_neighbor_set_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') {v w : V} :
⇑f w ∈ G'.neighbor_set (⇑f v) ↔ w ∈ G.neighbor_set v
source
@[simp]
theorem simple_graph.iso.map_edge_set_apply {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') (e : ↥(⇑simple_graph.edge_set G)) :
⇑(f.map_edge_set) e = ↑f.map_edge_set e
source
def simple_graph.iso.map_edge_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') :
↥(⇑simple_graph.edge_set G) ≃ ↥(⇑simple_graph.edge_set G')

An isomorphism of graphs induces an equivalence of edge sets.

Equations
source
@[simp]
theorem simple_graph.iso.map_edge_set_symm_apply {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') (e : ↥(⇑simple_graph.edge_set G')) :
⇑(f.map_edge_set.symm) e = ↑(f.symm).map_edge_set e
source
@[simp]
theorem simple_graph.iso.map_neighbor_set_symm_apply_coe {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') (v : V) (w : ↥(G'.neighbor_set (⇑f v))) :
↑(⇑((f.map_neighbor_set v).symm) w) = ⇑(f.symm) ↑w
source
def simple_graph.iso.map_neighbor_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') (v : V) :
↥(G.neighbor_set v) ≃ ↥(G'.neighbor_set (⇑f v))

A graph isomorphism induces an equivalence of neighbor sets.

Equations
source
@[simp]
theorem simple_graph.iso.map_neighbor_set_apply_coe {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') (v : V) (w : ↥(G.neighbor_set v)) :
↑(⇑(f.map_neighbor_set v) w) = ⇑f ↑w
source
theorem simple_graph.iso.card_eq_of_iso {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} [fintype V] [fintype W] (f : G ≃g G') :
fintype.card V = fintype.card W
source
@[protected]
def simple_graph.iso.comap {V : Type u} {W : Type v} (f : V ≃ W) (G : simple_graph W) :
simple_graph.comap ⇑(f.to_embedding) G ≃g G

Given a bijection, there is an embedding from the comapped graph into the original graph.

Equations
source
@[simp]
theorem simple_graph.iso.comap_apply {V : Type u} {W : Type v} (f : V ≃ W) (G : simple_graph W) (ᾰ : V) :
⇑(simple_graph.iso.comap f G) ᾰ = f.to_fun ᾰ
source
@[simp]
theorem simple_graph.iso.comap_symm_apply {V : Type u} {W : Type v} (f : V ≃ W) (G : simple_graph W) (ᾰ : W) :
⇑(rel_iso.symm (simple_graph.iso.comap f G)) ᾰ = f.inv_fun ᾰ
source
@[protected]
def simple_graph.iso.map {V : Type u} {W : Type v} (f : V ≃ W) (G : simple_graph V) :
G ≃g simple_graph.map f.to_embedding G

Given an injective function, there is an embedding from a graph into the mapped graph.

Equations
source
@[simp]
theorem simple_graph.iso.map_symm_apply {V : Type u} {W : Type v} (f : V ≃ W) (G : simple_graph V) (ᾰ : W) :
⇑(rel_iso.symm (simple_graph.iso.map f G)) ᾰ = f.inv_fun ᾰ
source
@[simp]
theorem simple_graph.iso.map_apply {V : Type u} {W : Type v} (f : V ≃ W) (G : simple_graph V) (ᾰ : V) :
⇑(simple_graph.iso.map f G) ᾰ = f.to_fun ᾰ
source
@[protected]
def simple_graph.iso.complete_graph {α : Type u_1} {β : Type u_2} (f : α ≃ β) :
⊤ ≃g ⊤

Equivalences of types induce isomorphisms of complete graphs on those types.

Equations
source
theorem simple_graph.iso.to_embedding_complete_graph {α : Type u_1} {β : Type u_2} (f : α ≃ β) :
(simple_graph.iso.complete_graph f).to_embedding = simple_graph.embedding.complete_graph f.to_embedding
source
@[reducible]
def simple_graph.iso.comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' ≃g G'') (f : G ≃g G') :
G ≃g G''

Composition of graph isomorphisms.

source
@[simp]
theorem simple_graph.iso.coe_comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' ≃g G'') (f : G ≃g G') :
⇑(f'.comp f) = ⇑f' ∘ ⇑f