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

• 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.neighborFinset is the Finset of vertices adjacent to a given vertex, if neighborSet is finite

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

• SimpleGraph.incidenceFinset is the Finset of edges containing a given vertex, if incidenceSet is finite

• SimpleGraph.Dart is an ordered pair of adjacent vertices, thought of as being an orientated edge. These are also known as "half-edges" or "bonds."

• SimpleGraph.Hom, SimpleGraph.Embedding, and SimpleGraph.Iso for graph homomorphisms, graph embeddings, and graph isomorphisms. Note that a graph embedding is a stronger notion than an injective graph homomorphism, since its image is an induced subgraph.

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

Notations

• →g, ↪g, and ≃g for graph homomorphisms, graph embeddings, and graph isomorphisms, respectively.

Implementation notes

• A locally finite graph is one with instances Π v, Fintype (G.neighborSet v).

• Given instances DecidableRel G.Adj and Fintype V, then the graph is locally finite, too.

• Morphisms of graphs are abbreviations for RelHom, RelEmbedding, and RelIso. To make use of pre-existing simp lemmas, definitions involving morphisms are abbreviations as well.

Naming Conventions

• If the vertex type of a graph is finite, we refer to its cardinality as CardVerts.

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.

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

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

structure SimpleGraph (V : Type u) : Type u

• Adj : V → V → Prop
• symm : Symmetric s.Adj
• loopless : Irreflexive s.Adj

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.

@[simp]

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

def SimpleGraph.mk' {V : Type u} : { adj // (∀ (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.

instance instFintypeSimpleGraph {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.

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 : V) (w : V) : SimpleGraph.Adj (SimpleGraph.fromRel r) v w ↔ v ≠ w ∧ (r v w ∨ r w v)

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

def emptyGraph (V : Type u) : SimpleGraph V

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

@[simp]

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

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 SimpleGraph.irrefl {V : Type u} (G : SimpleGraph V) {v : V} : ¬SimpleGraph.Adj G v v

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

@[simp]

theorem SimpleGraph.isSubgraph_eq_le {V : Type u} : SimpleGraph.IsSubgraph = fun x x_1 => x ≤ x_1

instance SimpleGraph.instSupSimpleGraph {V : Type u} : Sup (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 : SimpleGraph V) (y : SimpleGraph V) (v : V) (w : V) : SimpleGraph.Adj (x ⊔ y) v w ↔ SimpleGraph.Adj x v w ∨ SimpleGraph.Adj y v w

instance SimpleGraph.instInfSimpleGraph {V : Type u} : Inf (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 : SimpleGraph V) (y : SimpleGraph V) (v : V) (w : V) : SimpleGraph.Adj (x ⊓ y) v w ↔ SimpleGraph.Adj x v w ∧ SimpleGraph.Adj y 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 : V) (w : V) : SimpleGraph.Adj Gᶜ v w ↔ v ≠ w ∧ ¬SimpleGraph.Adj G 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 : SimpleGraph V) (y : SimpleGraph V) (v : V) (w : V) : SimpleGraph.Adj (x \ y) v w ↔ SimpleGraph.Adj x v w ∧ ¬SimpleGraph.Adj y 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 : V} {b : V} : SimpleGraph.Adj (sSup s) a b ↔ ∃ G, G ∈ s ∧ SimpleGraph.Adj G a b

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem SimpleGraph.iInf_adj_of_nonempty {ι : Sort u_1} {V : Type u} {a : V} {b : V} [Nonempty ι] {f : ι → SimpleGraph V} : SimpleGraph.Adj (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), SimpleGraph.Adj (f i) 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)

@[simp]

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

@[simp]

theorem SimpleGraph.bot_adj {V : Type u} (v : V) (w : V) : SimpleGraph.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 = ⊥

@[simp]

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

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

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

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

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

instance SimpleGraph.Sdiff.adjDecidable (V : Type u) (G : SimpleGraph V) (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 ∈ SimpleGraph.support G ↔ ∃ w, SimpleGraph.Adj G v w

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

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 => x ∈ SimpleGraph.neighborSet G v

def SimpleGraph.edgeSetEmbedding (V : Type u_3) : 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 refl. (That is, ⟦(v, w)⟧ ∈ G.edgeSet is definitionally equal to G.Adj v w.)

@[inline, reducible]

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 : V} {w : V} : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ SimpleGraph.edgeSet G ↔ SimpleGraph.Adj G v w

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

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

@[simp]

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

@[simp]

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

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

theorem SimpleGraph.edgeSet_mono {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} : G₁ ≤ G₂ → SimpleGraph.edgeSet G₁ ⊆ SimpleGraph.edgeSet G₂

Alias of the reverse direction of SimpleGraph.edgeSet_subset_edgeSet.

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

Alias of the reverse direction of SimpleGraph.edgeSet_ssubset_edgeSet.

@[simp]

theorem SimpleGraph.edgeSet_bot {V : Type u} : SimpleGraph.edgeSet ⊥ = ∅

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem SimpleGraph.edge_other_ne {V : Type u} (G : SimpleGraph V) {e : Sym2 V} (he : e ∈ SimpleGraph.edgeSet G) {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 => x ∈ SimpleGraph.edgeSet G

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Darts

structure SimpleGraph.Dart {V : Type u} (G : SimpleGraph V) extends Prod : Type u

• fst : V
• snd : V
• is_adj : SimpleGraph.Adj G s.fst s.snd

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

instance SimpleGraph.instDecidableEqDart : {V : Type u_3} → {G : SimpleGraph V} → [inst : DecidableEq V] → DecidableEq (SimpleGraph.Dart G)

theorem SimpleGraph.Dart.ext_iff {V : Type u} {G : SimpleGraph V} (d₁ : SimpleGraph.Dart G) (d₂ : SimpleGraph.Dart G) : d₁ = d₂ ↔ d₁.toProd = d₂.toProd

theorem SimpleGraph.Dart.ext {V : Type u} {G : SimpleGraph V} (d₁ : SimpleGraph.Dart G) (d₂ : SimpleGraph.Dart G) (h : d₁.toProd = d₂.toProd) : d₁ = d₂

theorem SimpleGraph.Dart.toProd_injective {V : Type u} {G : SimpleGraph V} : Function.Injective SimpleGraph.Dart.toProd

instance SimpleGraph.Dart.fintype {V : Type u} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] : Fintype (SimpleGraph.Dart G)

def SimpleGraph.Dart.edge {V : Type u} {G : SimpleGraph V} (d : SimpleGraph.Dart G) : Sym2 V

The edge associated to the dart.

@[simp]

theorem SimpleGraph.Dart.edge_mk {V : Type u} {G : SimpleGraph V} {p : V × V} (h : SimpleGraph.Adj G p.fst p.snd) : SimpleGraph.Dart.edge { toProd := p, is_adj := h } = Quotient.mk (Sym2.Rel.setoid V) p

@[simp]

theorem SimpleGraph.Dart.edge_mem {V : Type u} {G : SimpleGraph V} (d : SimpleGraph.Dart G) : SimpleGraph.Dart.edge d ∈ SimpleGraph.edgeSet G

@[simp]

theorem SimpleGraph.Dart.symm_toProd {V : Type u} {G : SimpleGraph V} (d : SimpleGraph.Dart G) : (SimpleGraph.Dart.symm d).toProd = Prod.swap d.toProd

def SimpleGraph.Dart.symm {V : Type u} {G : SimpleGraph V} (d : SimpleGraph.Dart G) : SimpleGraph.Dart G

The dart with reversed orientation from a given dart.

@[simp]

theorem SimpleGraph.Dart.symm_mk {V : Type u} {G : SimpleGraph V} {p : V × V} (h : SimpleGraph.Adj G p.fst p.snd) : SimpleGraph.Dart.symm { toProd := p, is_adj := h } = { toProd := Prod.swap p, is_adj := (_ : SimpleGraph.Adj G p.snd p.fst) }

@[simp]

theorem SimpleGraph.Dart.edge_symm {V : Type u} {G : SimpleGraph V} (d : SimpleGraph.Dart G) : SimpleGraph.Dart.edge (SimpleGraph.Dart.symm d) = SimpleGraph.Dart.edge d

@[simp]

theorem SimpleGraph.Dart.edge_comp_symm {V : Type u} {G : SimpleGraph V} : SimpleGraph.Dart.edge ∘ SimpleGraph.Dart.symm = SimpleGraph.Dart.edge

@[simp]

theorem SimpleGraph.Dart.symm_symm {V : Type u} {G : SimpleGraph V} (d : SimpleGraph.Dart G) : SimpleGraph.Dart.symm (SimpleGraph.Dart.symm d) = d

@[simp]

theorem SimpleGraph.Dart.symm_involutive {V : Type u} {G : SimpleGraph V} : Function.Involutive SimpleGraph.Dart.symm

theorem SimpleGraph.Dart.symm_ne {V : Type u} {G : SimpleGraph V} (d : SimpleGraph.Dart G) : SimpleGraph.Dart.symm d ≠ d

theorem SimpleGraph.dart_edge_eq_iff {V : Type u} {G : SimpleGraph V} (d₁ : SimpleGraph.Dart G) (d₂ : SimpleGraph.Dart G) : SimpleGraph.Dart.edge d₁ = SimpleGraph.Dart.edge d₂ ↔ d₁ = d₂ ∨ d₁ = SimpleGraph.Dart.symm d₂

theorem SimpleGraph.dart_edge_eq_mk'_iff {V : Type u} {G : SimpleGraph V} {d : SimpleGraph.Dart G} {p : V × V} : SimpleGraph.Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) p ↔ d.toProd = p ∨ d.toProd = Prod.swap p

theorem SimpleGraph.dart_edge_eq_mk'_iff' {V : Type u} {G : SimpleGraph V} {d : SimpleGraph.Dart G} {u : V} {v : V} : SimpleGraph.Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (u, v) ↔ d.fst = u ∧ d.snd = v ∨ d.fst = v ∧ d.snd = u

def SimpleGraph.DartAdj {V : Type u} (G : SimpleGraph V) (d : SimpleGraph.Dart G) (d' : SimpleGraph.Dart G) : 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.

@[simp]

theorem SimpleGraph.dartOfNeighborSet_toProd {V : Type u} (G : SimpleGraph V) (v : V) (w : ↑(SimpleGraph.neighborSet G v)) : (SimpleGraph.dartOfNeighborSet G v w).toProd = (v, ↑w)

def SimpleGraph.dartOfNeighborSet {V : Type u} (G : SimpleGraph V) (v : V) (w : ↑(SimpleGraph.neighborSet G v)) : SimpleGraph.Dart G

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

theorem SimpleGraph.dartOfNeighborSet_injective {V : Type u} (G : SimpleGraph V) (v : V) : Function.Injective (SimpleGraph.dartOfNeighborSet G v)

instance SimpleGraph.nonempty_dart_top {V : Type u} [Nontrivial V] : Nonempty (SimpleGraph.Dart ⊤)

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) : SimpleGraph.incidenceSet G v ⊆ SimpleGraph.edgeSet G

theorem SimpleGraph.mk'_mem_incidenceSet_iff {V : Type u} (G : SimpleGraph V) {a : V} {b : V} {c : V} : Quotient.mk (Sym2.Rel.setoid V) (b, c) ∈ SimpleGraph.incidenceSet G a ↔ SimpleGraph.Adj G b c ∧ (a = b ∨ a = c)

theorem SimpleGraph.mk'_mem_incidenceSet_left_iff {V : Type u} (G : SimpleGraph V) {a : V} {b : V} : Quotient.mk (Sym2.Rel.setoid V) (a, b) ∈ SimpleGraph.incidenceSet G a ↔ SimpleGraph.Adj G a b

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

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

theorem SimpleGraph.incidenceSet_inter_incidenceSet_subset {V : Type u} (G : SimpleGraph V) {a : V} {b : V} (h : a ≠ b) : SimpleGraph.incidenceSet G a ∩ SimpleGraph.incidenceSet G b ⊆ {Quotient.mk (Sym2.Rel.setoid V) (a, b)}

theorem SimpleGraph.incidenceSet_inter_incidenceSet_of_adj {V : Type u} (G : SimpleGraph V) {a : V} {b : V} (h : SimpleGraph.Adj G a b) : SimpleGraph.incidenceSet G a ∩ SimpleGraph.incidenceSet G b = {Quotient.mk (Sym2.Rel.setoid V) (a, b)}

theorem SimpleGraph.adj_of_mem_incidenceSet {V : Type u} (G : SimpleGraph V) {a : V} {b : V} {e : Sym2 V} (h : a ≠ b) (ha : e ∈ SimpleGraph.incidenceSet G a) (hb : e ∈ SimpleGraph.incidenceSet G b) : SimpleGraph.Adj G a b

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

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

@[reducible]

def SimpleGraph.edgeFinset {V : Type u} (G : SimpleGraph V) [Fintype ↑(SimpleGraph.edgeSet G)] : Finset (Sym2 V)

The edgeSet of the graph as a Finset.

theorem SimpleGraph.coe_edgeFinset {V : Type u} (G : SimpleGraph V) [Fintype ↑(SimpleGraph.edgeSet G)] : ↑(SimpleGraph.edgeFinset G) = SimpleGraph.edgeSet G

theorem SimpleGraph.mem_edgeFinset {V : Type u} {G : SimpleGraph V} {e : Sym2 V} [Fintype ↑(SimpleGraph.edgeSet G)] : e ∈ SimpleGraph.edgeFinset G ↔ e ∈ SimpleGraph.edgeSet G

theorem SimpleGraph.not_isDiag_of_mem_edgeFinset {V : Type u} {G : SimpleGraph V} {e : Sym2 V} [Fintype ↑(SimpleGraph.edgeSet G)] : e ∈ SimpleGraph.edgeFinset G → ¬Sym2.IsDiag e

theorem SimpleGraph.edgeFinset_inj {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype ↑(SimpleGraph.edgeSet G₁)] [Fintype ↑(SimpleGraph.edgeSet G₂)] : SimpleGraph.edgeFinset G₁ = SimpleGraph.edgeFinset G₂ ↔ G₁ = G₂

theorem SimpleGraph.edgeFinset_subset_edgeFinset {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype ↑(SimpleGraph.edgeSet G₁)] [Fintype ↑(SimpleGraph.edgeSet G₂)] : SimpleGraph.edgeFinset G₁ ⊆ SimpleGraph.edgeFinset G₂ ↔ G₁ ≤ G₂

theorem SimpleGraph.edgeFinset_ssubset_edgeFinset {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype ↑(SimpleGraph.edgeSet G₁)] [Fintype ↑(SimpleGraph.edgeSet G₂)] : SimpleGraph.edgeFinset G₁ ⊂ SimpleGraph.edgeFinset G₂ ↔ G₁ < G₂

theorem SimpleGraph.edgeFinset_mono {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype ↑(SimpleGraph.edgeSet G₁)] [Fintype ↑(SimpleGraph.edgeSet G₂)] : G₁ ≤ G₂ → SimpleGraph.edgeFinset G₁ ⊆ SimpleGraph.edgeFinset G₂

Alias of the reverse direction of SimpleGraph.edgeFinset_subset_edgeFinset.

theorem SimpleGraph.edgeFinset_strict_mono {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype ↑(SimpleGraph.edgeSet G₁)] [Fintype ↑(SimpleGraph.edgeSet G₂)] : G₁ < G₂ → SimpleGraph.edgeFinset G₁ ⊂ SimpleGraph.edgeFinset G₂

Alias of the reverse direction of SimpleGraph.edgeFinset_ssubset_edgeFinset.

@[simp]

theorem SimpleGraph.edgeFinset_bot {V : Type u} : SimpleGraph.edgeFinset ⊥ = ∅

@[simp]

theorem SimpleGraph.edgeFinset_sup {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype ↑(SimpleGraph.edgeSet G₁)] [Fintype ↑(SimpleGraph.edgeSet G₂)] [DecidableEq V] : SimpleGraph.edgeFinset (G₁ ⊔ G₂) = SimpleGraph.edgeFinset G₁ ∪ SimpleGraph.edgeFinset G₂

@[simp]

theorem SimpleGraph.edgeFinset_inf {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype ↑(SimpleGraph.edgeSet G₁)] [Fintype ↑(SimpleGraph.edgeSet G₂)] [DecidableEq V] : SimpleGraph.edgeFinset (G₁ ⊓ G₂) = SimpleGraph.edgeFinset G₁ ∩ SimpleGraph.edgeFinset G₂

@[simp]

theorem SimpleGraph.edgeFinset_sdiff {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype ↑(SimpleGraph.edgeSet G₁)] [Fintype ↑(SimpleGraph.edgeSet G₂)] [DecidableEq V] : SimpleGraph.edgeFinset (G₁ \ G₂) = SimpleGraph.edgeFinset G₁ \ SimpleGraph.edgeFinset G₂

theorem SimpleGraph.edgeFinset_card {V : Type u} {G : SimpleGraph V} [Fintype ↑(SimpleGraph.edgeSet G)] : Finset.card (SimpleGraph.edgeFinset G) = Fintype.card ↑(SimpleGraph.edgeSet G)

@[simp]

theorem SimpleGraph.edgeSet_univ_card {V : Type u} {G : SimpleGraph V} [Fintype ↑(SimpleGraph.edgeSet G)] : Finset.card Finset.univ = Finset.card (SimpleGraph.edgeFinset G)

@[simp]

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

@[simp]

theorem SimpleGraph.mem_incidenceSet {V : Type u} (G : SimpleGraph V) (v : V) (w : V) : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ SimpleGraph.incidenceSet G v ↔ SimpleGraph.Adj G v w

theorem SimpleGraph.mem_incidence_iff_neighbor {V : Type u} (G : SimpleGraph V) {v : V} {w : V} : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ SimpleGraph.incidenceSet G v ↔ w ∈ SimpleGraph.neighborSet G v

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

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

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

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

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

def SimpleGraph.commonNeighbors {V : Type u} (G : SimpleGraph V) (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 : V) (w : V) : SimpleGraph.commonNeighbors G v w = SimpleGraph.neighborSet G v ∩ SimpleGraph.neighborSet G w

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

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

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

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

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

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

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

theorem SimpleGraph.commonNeighbors_top_eq {V : Type u} {v : V} {w : V} : SimpleGraph.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 ∈ SimpleGraph.incidenceSet G 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 ∈ SimpleGraph.incidenceSet G v) : e ∈ SimpleGraph.incidenceSet G (SimpleGraph.otherVertexOfIncident G h)

theorem SimpleGraph.incidence_other_prop {V : Type u} (G : SimpleGraph V) [DecidableEq V] {v : V} {e : Sym2 V} (h : e ∈ SimpleGraph.incidenceSet G v) : SimpleGraph.otherVertexOfIncident G h ∈ SimpleGraph.neighborSet G v

theorem SimpleGraph.incidence_other_neighbor_edge {V : Type u} (G : SimpleGraph V) [DecidableEq V] {v : V} {w : V} (h : w ∈ SimpleGraph.neighborSet G v) : SimpleGraph.otherVertexOfIncident G (_ : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ SimpleGraph.incidenceSet G v) = w

@[simp]

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

@[simp]

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

def SimpleGraph.incidenceSetEquivNeighborSet {V : Type u} (G : SimpleGraph V) [DecidableEq V] (v : V) : ↑(SimpleGraph.incidenceSet G v) ≃ ↑(SimpleGraph.neighborSet G v)

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

Edge deletion

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

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

See also: SimpleGraph.Subgraph.deleteEdges.

@[simp]

theorem SimpleGraph.deleteEdges_adj {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) (v : V) (w : V) : SimpleGraph.Adj (SimpleGraph.deleteEdges G s) v w ↔ SimpleGraph.Adj G v w ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s

theorem SimpleGraph.sdiff_eq_deleteEdges {V : Type u} (G : SimpleGraph V) (G' : SimpleGraph V) : G \ G' = SimpleGraph.deleteEdges G (SimpleGraph.edgeSet G')

theorem SimpleGraph.deleteEdges_eq_sdiff_fromEdgeSet {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) : SimpleGraph.deleteEdges G s = G \ SimpleGraph.fromEdgeSet s

theorem SimpleGraph.compl_eq_deleteEdges {V : Type u} (G : SimpleGraph V) : Gᶜ = SimpleGraph.deleteEdges ⊤ (SimpleGraph.edgeSet G)

@[simp]

theorem SimpleGraph.deleteEdges_deleteEdges {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) (s' : Set (Sym2 V)) : SimpleGraph.deleteEdges (SimpleGraph.deleteEdges G s) s' = SimpleGraph.deleteEdges G (s ∪ s')

@[simp]

theorem SimpleGraph.deleteEdges_empty_eq {V : Type u} (G : SimpleGraph V) : SimpleGraph.deleteEdges G ∅ = G

@[simp]

theorem SimpleGraph.deleteEdges_univ_eq {V : Type u} (G : SimpleGraph V) : SimpleGraph.deleteEdges G Set.univ = ⊥

theorem SimpleGraph.deleteEdges_le {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) : SimpleGraph.deleteEdges G s ≤ G

theorem SimpleGraph.deleteEdges_le_of_le {V : Type u} (G : SimpleGraph V) {s : Set (Sym2 V)} {s' : Set (Sym2 V)} (h : s ⊆ s') : SimpleGraph.deleteEdges G s' ≤ SimpleGraph.deleteEdges G s

theorem SimpleGraph.deleteEdges_eq_inter_edgeSet {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) : SimpleGraph.deleteEdges G s = SimpleGraph.deleteEdges G (s ∩ SimpleGraph.edgeSet G)

theorem SimpleGraph.deleteEdges_sdiff_eq_of_le {V : Type u} (G : SimpleGraph V) {H : SimpleGraph V} (h : H ≤ G) : SimpleGraph.deleteEdges G (SimpleGraph.edgeSet G \ SimpleGraph.edgeSet H) = H

theorem SimpleGraph.edgeSet_deleteEdges {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) : SimpleGraph.edgeSet (SimpleGraph.deleteEdges G s) = SimpleGraph.edgeSet G \ s

theorem SimpleGraph.edgeFinset_deleteEdges {V : Type u} (G : SimpleGraph V) [Fintype (Sym2 V)] [DecidableEq V] [DecidableRel G.Adj] (s : Finset (Sym2 V)) [DecidableRel (SimpleGraph.deleteEdges G ↑s).Adj] : SimpleGraph.edgeFinset (SimpleGraph.deleteEdges G ↑s) = SimpleGraph.edgeFinset G \ s

def SimpleGraph.DeleteFar {𝕜 : Type u_2} {V : Type u} (G : SimpleGraph V) [OrderedRing 𝕜] [Fintype (Sym2 V)] [DecidableRel G.Adj] (p : SimpleGraph 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.

theorem SimpleGraph.deleteFar_iff {𝕜 : Type u_2} {V : Type u} {G : SimpleGraph V} [OrderedRing 𝕜] [Fintype (Sym2 V)] [DecidableEq V] [DecidableRel G.Adj] {p : SimpleGraph V → Prop} {r : 𝕜} : SimpleGraph.DeleteFar G p r ↔ ∀ ⦃H : SimpleGraph V⦄, H ≤ G → p H → r ≤ ↑(Finset.card (SimpleGraph.edgeFinset G)) - ↑(Finset.card (SimpleGraph.edgeFinset H))

theorem SimpleGraph.DeleteFar.le_card_sub_card {𝕜 : Type u_2} {V : Type u} {G : SimpleGraph V} [OrderedRing 𝕜] [Fintype (Sym2 V)] [DecidableEq V] [DecidableRel G.Adj] {p : SimpleGraph V → Prop} {r : 𝕜} : SimpleGraph.DeleteFar G p r → ∀ ⦃H : SimpleGraph V⦄, H ≤ G → p H → r ≤ ↑(Finset.card (SimpleGraph.edgeFinset G)) - ↑(Finset.card (SimpleGraph.edgeFinset H))

Alias of the forward direction of SimpleGraph.deleteFar_iff.

theorem SimpleGraph.DeleteFar.mono {𝕜 : Type u_2} {V : Type u} {G : SimpleGraph V} [OrderedRing 𝕜] [Fintype (Sym2 V)] [DecidableRel G.Adj] {p : SimpleGraph V → Prop} {r₁ : 𝕜} {r₂ : 𝕜} (h : SimpleGraph.DeleteFar G p r₂) (hr : r₁ ≤ r₂) : SimpleGraph.DeleteFar G p r₁

Map and comap

def SimpleGraph.map {V : Type u} {W : Type v} (f : V ↪ W) (G : SimpleGraph V) : SimpleGraph W

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

This is injective (see SimpleGraph.map_injective).

@[simp]

theorem SimpleGraph.map_adj {V : Type u} {W : Type v} (f : V ↪ W) (G : SimpleGraph V) (u : W) (v : W) : SimpleGraph.Adj (SimpleGraph.map f G) u v ↔ ∃ u' v', SimpleGraph.Adj G u' v' ∧ ↑f u' = u ∧ ↑f v' = v

theorem SimpleGraph.map_monotone {V : Type u} {W : Type v} (f : V ↪ W) : Monotone (SimpleGraph.map f)

@[simp]

theorem SimpleGraph.comap_Adj {V : Type u} {W : Type v} (f : V → W) (G : SimpleGraph W) (u : V) (v : V) : SimpleGraph.Adj (SimpleGraph.comap f G) u v = SimpleGraph.Adj G (f u) (f v)

def SimpleGraph.comap {V : Type u} {W : Type v} (f : V → W) (G : SimpleGraph W) : SimpleGraph 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 SimpleGraph.induce for a wrapper.

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

theorem SimpleGraph.comap_monotone {V : Type u} {W : Type v} (f : V ↪ W) : Monotone (SimpleGraph.comap ↑f)

@[simp]

theorem SimpleGraph.comap_map_eq {V : Type u} {W : Type v} (f : V ↪ W) (G : SimpleGraph V) : SimpleGraph.comap (↑f) (SimpleGraph.map f G) = G

theorem SimpleGraph.leftInverse_comap_map {V : Type u} {W : Type v} (f : V ↪ W) : Function.LeftInverse (SimpleGraph.comap ↑f) (SimpleGraph.map f)

theorem SimpleGraph.map_injective {V : Type u} {W : Type v} (f : V ↪ W) : Function.Injective (SimpleGraph.map f)

theorem SimpleGraph.comap_surjective {V : Type u} {W : Type v} (f : V ↪ W) : Function.Surjective (SimpleGraph.comap ↑f)

theorem SimpleGraph.map_le_iff_le_comap {V : Type u} {W : Type v} (f : V ↪ W) (G : SimpleGraph V) (G' : SimpleGraph W) : SimpleGraph.map f G ≤ G' ↔ G ≤ SimpleGraph.comap (↑f) G'

theorem SimpleGraph.map_comap_le {V : Type u} {W : Type v} (f : V ↪ W) (G : SimpleGraph W) : SimpleGraph.map f (SimpleGraph.comap (↑f) G) ≤ G

theorem SimpleGraph.le_comap_of_subsingleton {V : Type u} {W : Type v} (G : SimpleGraph V) (G' : SimpleGraph W) (f : V → W) [Subsingleton V] : G ≤ SimpleGraph.comap f G'

theorem SimpleGraph.map_le_of_subsingleton {V : Type u} {W : Type v} (G : SimpleGraph V) (G' : SimpleGraph W) (f : V ↪ W) [Subsingleton V] : SimpleGraph.map f G ≤ G'

@[inline, reducible]

abbrev SimpleGraph.completeMultipartiteGraph {ι : Type u_3} (V : ι → Type u_4) : SimpleGraph ((i : ι) × V i)

Given a family of vertex types indexed by ι, pulling back from ⊤ : SimpleGraph ι yields the complete multipartite graph on the family. Two vertices are adjacent if and only if their indices are not equal.

Induced graphs

@[reducible]

def SimpleGraph.induce {V : Type u} (s : Set V) (G : SimpleGraph V) : SimpleGraph ↑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 SimpleGraph.comap.

@[simp]

theorem SimpleGraph.induce_singleton_eq_top {V : Type u} (G : SimpleGraph V) (v : V) : SimpleGraph.induce {v} G = ⊤

@[reducible]

def SimpleGraph.spanningCoe {V : Type u} {s : Set V} (G : SimpleGraph ↑s) : SimpleGraph V

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

theorem SimpleGraph.induce_spanningCoe {V : Type u} {s : Set V} {G : SimpleGraph ↑s} : SimpleGraph.induce s (SimpleGraph.spanningCoe G) = G

theorem SimpleGraph.spanningCoe_induce_le {V : Type u} (G : SimpleGraph V) (s : Set V) : SimpleGraph.spanningCoe (SimpleGraph.induce s G) ≤ 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.neighborSet v).

We define G.neighborFinset v to be the Finset version of G.neighborSet v. Use neighborFinset_eq_filter to rewrite this definition as a Finset.filter expression.

def SimpleGraph.neighborFinset {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] : Finset V

G.neighbors v is the Finset version of G.Adj v in case G is locally finite at v.

theorem SimpleGraph.neighborFinset_def {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] : SimpleGraph.neighborFinset G v = Set.toFinset (SimpleGraph.neighborSet G v)

@[simp]

theorem SimpleGraph.mem_neighborFinset {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] (w : V) : w ∈ SimpleGraph.neighborFinset G v ↔ SimpleGraph.Adj G v w

theorem SimpleGraph.not_mem_neighborFinset_self {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] : ¬v ∈ SimpleGraph.neighborFinset G v

theorem SimpleGraph.neighborFinset_disjoint_singleton {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] : Disjoint (SimpleGraph.neighborFinset G v) {v}

theorem SimpleGraph.singleton_disjoint_neighborFinset {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] : Disjoint {v} (SimpleGraph.neighborFinset G v)

def SimpleGraph.degree {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] : ℕ

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

@[simp]

theorem SimpleGraph.card_neighborFinset_eq_degree {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] : Finset.card (SimpleGraph.neighborFinset G v) = SimpleGraph.degree G v

@[simp]

theorem SimpleGraph.card_neighborSet_eq_degree {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] : Fintype.card ↑(SimpleGraph.neighborSet G v) = SimpleGraph.degree G v

theorem SimpleGraph.degree_pos_iff_exists_adj {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] : 0 < SimpleGraph.degree G v ↔ ∃ w, SimpleGraph.Adj G v w

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

instance SimpleGraph.incidenceSetFintype {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] [DecidableEq V] : Fintype ↑(SimpleGraph.incidenceSet G v)

def SimpleGraph.incidenceFinset {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] [DecidableEq V] : Finset (Sym2 V)

This is the Finset version of incidenceSet.

@[simp]

theorem SimpleGraph.card_incidenceSet_eq_degree {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] [DecidableEq V] : Fintype.card ↑(SimpleGraph.incidenceSet G v) = SimpleGraph.degree G v

@[simp]

theorem SimpleGraph.card_incidenceFinset_eq_degree {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] [DecidableEq V] : Finset.card (SimpleGraph.incidenceFinset G v) = SimpleGraph.degree G v

@[simp]

theorem SimpleGraph.mem_incidenceFinset {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] [DecidableEq V] (e : Sym2 V) : e ∈ SimpleGraph.incidenceFinset G v ↔ e ∈ SimpleGraph.incidenceSet G v

theorem SimpleGraph.incidenceFinset_eq_filter {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(SimpleGraph.neighborSet G v)] [DecidableEq V] [Fintype ↑(SimpleGraph.edgeSet G)] : SimpleGraph.incidenceFinset G v = Finset.filter (Membership.mem v) (SimpleGraph.edgeFinset G)

@[reducible]

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

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

def SimpleGraph.IsRegularOfDegree {V : Type u} (G : SimpleGraph V) [SimpleGraph.LocallyFinite G] (d : ℕ) : Prop

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

theorem SimpleGraph.IsRegularOfDegree.degree_eq {V : Type u} {G : SimpleGraph V} [SimpleGraph.LocallyFinite G] {d : ℕ} (h : SimpleGraph.IsRegularOfDegree G d) (v : V) : SimpleGraph.degree G v = d

theorem SimpleGraph.IsRegularOfDegree.compl {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} (h : SimpleGraph.IsRegularOfDegree G k) : SimpleGraph.IsRegularOfDegree Gᶜ (Fintype.card V - 1 - k)

instance SimpleGraph.neighborSetFintype {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) : Fintype ↑(SimpleGraph.neighborSet G v)

theorem SimpleGraph.neighborFinset_eq_filter {V : Type u} (G : SimpleGraph V) [Fintype V] {v : V} [DecidableRel G.Adj] : SimpleGraph.neighborFinset G v = Finset.filter (SimpleGraph.Adj G v) Finset.univ

theorem SimpleGraph.neighborFinset_compl {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (v : V) : SimpleGraph.neighborFinset Gᶜ v = (SimpleGraph.neighborFinset G v)ᶜ \ {v}

@[simp]

theorem SimpleGraph.complete_graph_degree {V : Type u} [Fintype V] [DecidableEq V] (v : V) : SimpleGraph.degree ⊤ v = Fintype.card V - 1

theorem SimpleGraph.bot_degree {V : Type u} [Fintype V] (v : V) : SimpleGraph.degree ⊥ v = 0

theorem SimpleGraph.IsRegularOfDegree.top {V : Type u} [Fintype V] [DecidableEq V] : SimpleGraph.IsRegularOfDegree ⊤ (Fintype.card V - 1)

def SimpleGraph.minDegree {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel 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, minDegree_le_degree and le_minDegree_of_forall_le_degree.

theorem SimpleGraph.exists_minimal_degree_vertex {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Nonempty V] : ∃ v, SimpleGraph.minDegree G = SimpleGraph.degree G v

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

theorem SimpleGraph.minDegree_le_degree {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) : SimpleGraph.minDegree G ≤ SimpleGraph.degree G v

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

theorem SimpleGraph.le_minDegree_of_forall_le_degree {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Nonempty V] (k : ℕ) (h : ∀ (v : V), k ≤ SimpleGraph.degree G v) : k ≤ SimpleGraph.minDegree G

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.minDegree is defined to be a natural.

def SimpleGraph.maxDegree {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel 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_maxDegree and maxDegree_le_of_forall_degree_le.

theorem SimpleGraph.exists_maximal_degree_vertex {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Nonempty V] : ∃ v, SimpleGraph.maxDegree G = SimpleGraph.degree G v

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

theorem SimpleGraph.degree_le_maxDegree {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) : SimpleGraph.degree G v ≤ SimpleGraph.maxDegree G

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

theorem SimpleGraph.maxDegree_le_of_forall_degree_le {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (k : ℕ) (h : ∀ (v : V), SimpleGraph.degree G v ≤ k) : SimpleGraph.maxDegree G ≤ k

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

theorem SimpleGraph.degree_lt_card_verts {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) : SimpleGraph.degree G v < Fintype.card V

theorem SimpleGraph.maxDegree_lt_card_verts {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Nonempty V] : SimpleGraph.maxDegree G < 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.

theorem SimpleGraph.card_commonNeighbors_le_degree_left {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) (w : V) : Fintype.card ↑(SimpleGraph.commonNeighbors G v w) ≤ SimpleGraph.degree G v

theorem SimpleGraph.card_commonNeighbors_le_degree_right {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) (w : V) : Fintype.card ↑(SimpleGraph.commonNeighbors G v w) ≤ SimpleGraph.degree G w

theorem SimpleGraph.card_commonNeighbors_lt_card_verts {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) (w : V) : Fintype.card ↑(SimpleGraph.commonNeighbors G v w) < Fintype.card V

theorem SimpleGraph.Adj.card_commonNeighbors_lt_degree {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} {w : V} (h : SimpleGraph.Adj G v w) : Fintype.card ↑(SimpleGraph.commonNeighbors G v w) < SimpleGraph.degree G v

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

theorem SimpleGraph.card_commonNeighbors_top {V : Type u} [Fintype V] [DecidableEq V] {v : V} {w : V} (h : v ≠ w) : Fintype.card ↑(SimpleGraph.commonNeighbors ⊤ v w) = Fintype.card V - 2

@[inline, reducible]

abbrev SimpleGraph.Hom {V : Type u} {W : Type v} (G : SimpleGraph V) (G' : SimpleGraph 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.

@[inline, reducible]

abbrev SimpleGraph.Embedding {V : Type u} {W : Type v} (G : SimpleGraph V) (G' : SimpleGraph 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.

@[inline, reducible]

abbrev SimpleGraph.Iso {V : Type u} {W : Type v} (G : SimpleGraph V) (G' : SimpleGraph W) : Type (max u v)

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

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

def SimpleGraph.«term_→g_» : Lean.TrailingParserDescr

def SimpleGraph.«term_↪g_» : Lean.TrailingParserDescr

def SimpleGraph.«term_≃g_» : Lean.TrailingParserDescr

@[inline, reducible]

abbrev SimpleGraph.Hom.id {V : Type u} {G : SimpleGraph V} : G →g G

The identity homomorphism from a graph to itself.

theorem SimpleGraph.Hom.map_adj {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V} {w : V} (h : SimpleGraph.Adj G v w) : SimpleGraph.Adj G' (↑f v) (↑f w)

theorem SimpleGraph.Hom.map_mem_edgeSet {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {e : Sym2 V} (h : e ∈ SimpleGraph.edgeSet G) : Sym2.map (↑f) e ∈ SimpleGraph.edgeSet G'

theorem SimpleGraph.Hom.apply_mem_neighborSet {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V} {w : V} (h : w ∈ SimpleGraph.neighborSet G v) : ↑f w ∈ SimpleGraph.neighborSet G' (↑f v)

@[simp]

theorem SimpleGraph.Hom.mapEdgeSet_coe {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (e : ↑(SimpleGraph.edgeSet G)) : ↑(SimpleGraph.Hom.mapEdgeSet f e) = Sym2.map ↑f ↑e

def SimpleGraph.Hom.mapEdgeSet {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (e : ↑(SimpleGraph.edgeSet G)) : ↑(SimpleGraph.edgeSet G')

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

@[simp]

theorem SimpleGraph.Hom.mapNeighborSet_coe {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (v : V) (w : ↑(SimpleGraph.neighborSet G v)) : ↑(SimpleGraph.Hom.mapNeighborSet f v w) = ↑f ↑w

def SimpleGraph.Hom.mapNeighborSet {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (v : V) (w : ↑(SimpleGraph.neighborSet G v)) : ↑(SimpleGraph.neighborSet G' (↑f v))

The map between neighbor sets induced by a homomorphism.

def SimpleGraph.Hom.mapDart {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (d : SimpleGraph.Dart G) : SimpleGraph.Dart G'

The map between darts induced by a homomorphism.

@[simp]

theorem SimpleGraph.Hom.mapDart_apply {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (d : SimpleGraph.Dart G) : SimpleGraph.Hom.mapDart f d = { toProd := Prod.map (↑f) (↑f) d.toProd, is_adj := (_ : SimpleGraph.Adj G' (↑f d.1.fst) (↑f d.1.snd)) }

@[simp]

theorem SimpleGraph.Hom.mapSpanningSubgraphs_apply {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') (x : V) : ↑(SimpleGraph.Hom.mapSpanningSubgraphs h) x = x

def SimpleGraph.Hom.mapSpanningSubgraphs {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') : G →g G'

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

theorem SimpleGraph.Hom.mapEdgeSet.injective {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (hinj : Function.Injective ↑f) : Function.Injective (SimpleGraph.Hom.mapEdgeSet f)

theorem SimpleGraph.Hom.injective_of_top_hom {V : Type u} {W : Type v} {G' : SimpleGraph W} (f : ⊤ →g G') : Function.Injective ↑f

Every graph homomorphism from a complete graph is injective.

@[simp]

theorem SimpleGraph.Hom.comap_apply {V : Type u} {W : Type v} (f : V → W) (G : SimpleGraph W) : ∀ (a : V), ↑(SimpleGraph.Hom.comap f G) a = f a

def SimpleGraph.Hom.comap {V : Type u} {W : Type v} (f : V → W) (G : SimpleGraph W) : SimpleGraph.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 SimpleGraph.Embedding.comap).

@[inline, reducible]

abbrev SimpleGraph.Hom.comp {V : Type u} {W : Type v} {X : Type w} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' →g G'') (f : G →g G') : G →g G''

Composition of graph homomorphisms.

@[simp]

theorem SimpleGraph.Hom.coe_comp {V : Type u} {W : Type v} {X : Type w} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' →g G'') (f : G →g G') : ↑(SimpleGraph.Hom.comp f' f) = ↑f' ∘ ↑f

@[inline, reducible]

abbrev SimpleGraph.Embedding.refl {V : Type u} {G : SimpleGraph V} : G ↪g G

The identity embedding from a graph to itself.

@[inline, reducible]

abbrev SimpleGraph.Embedding.toHom {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') : G →g G'

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

theorem SimpleGraph.Embedding.map_adj_iff {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {v : V} {w : V} : SimpleGraph.Adj G' (↑f v) (↑f w) ↔ SimpleGraph.Adj G v w

theorem SimpleGraph.Embedding.map_mem_edgeSet_iff {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {e : Sym2 V} : Sym2.map (↑f) e ∈ SimpleGraph.edgeSet G' ↔ e ∈ SimpleGraph.edgeSet G

theorem SimpleGraph.Embedding.apply_mem_neighborSet_iff {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {v : V} {w : V} : ↑f w ∈ SimpleGraph.neighborSet G' (↑f v) ↔ w ∈ SimpleGraph.neighborSet G v

@[simp]

theorem SimpleGraph.Embedding.mapEdgeSet_apply {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (e : ↑(SimpleGraph.edgeSet G)) : ↑(SimpleGraph.Embedding.mapEdgeSet f) e = SimpleGraph.Hom.mapEdgeSet (RelEmbedding.toRelHom f) e

def SimpleGraph.Embedding.mapEdgeSet {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') : ↑(SimpleGraph.edgeSet G) ↪ ↑(SimpleGraph.edgeSet G')

A graph embedding induces an embedding of edge sets.

@[simp]

theorem SimpleGraph.Embedding.mapNeighborSet_apply_coe {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (v : V) (w : ↑(SimpleGraph.neighborSet G v)) : ↑(↑(SimpleGraph.Embedding.mapNeighborSet f v) w) = ↑f ↑w

def SimpleGraph.Embedding.mapNeighborSet {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (v : V) : ↑(SimpleGraph.neighborSet G v) ↪ ↑(SimpleGraph.neighborSet G' (↑f v))

A graph embedding induces an embedding of neighbor sets.

def SimpleGraph.Embedding.comap {V : Type u} {W : Type v} (f : V ↪ W) (G : SimpleGraph W) : SimpleGraph.comap (↑f) G ↪g G

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

@[simp]

theorem SimpleGraph.Embedding.comap_apply {V : Type u} {W : Type v} (f : V ↪ W) (G : SimpleGraph W) (v : V) : ↑(SimpleGraph.Embedding.comap f G) v = ↑f v

def SimpleGraph.Embedding.map {V : Type u} {W : Type v} (f : V ↪ W) (G : SimpleGraph V) : G ↪g SimpleGraph.map f G

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

@[simp]

theorem SimpleGraph.Embedding.map_apply {V : Type u} {W : Type v} (f : V ↪ W) (G : SimpleGraph V) (v : V) : ↑(SimpleGraph.Embedding.map f G) v = ↑f v

@[reducible]

def SimpleGraph.Embedding.induce {V : Type u} {G : SimpleGraph V} (s : Set V) : SimpleGraph.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.

@[reducible]

def SimpleGraph.Embedding.spanningCoe {V : Type u} {s : Set V} (G : SimpleGraph ↑s) : G ↪g SimpleGraph.spanningCoe G

Graphs on a set of vertices embed in their spanningCoe.

def SimpleGraph.Embedding.completeGraph {α : Type u_3} {β : Type u_4} (f : α ↪ β) : ⊤ ↪g ⊤

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

@[inline, reducible]

abbrev SimpleGraph.Embedding.comp {V : Type u} {W : Type v} {X : Type w} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ↪g G'') (f : G ↪g G') : G ↪g G''

Composition of graph embeddings.

@[simp]

theorem SimpleGraph.Embedding.coe_comp {V : Type u} {W : Type v} {X : Type w} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ↪g G'') (f : G ↪g G') : ↑(SimpleGraph.Embedding.comp f' f) = ↑f' ∘ ↑f

def SimpleGraph.induceHom {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (↑φ) s t) : SimpleGraph.induce s G →g SimpleGraph.induce t G'

The restriction of a morphism of graphs to induced subgraphs.

@[simp]

theorem SimpleGraph.coe_induceHom {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (↑φ) s t) : ↑(SimpleGraph.induceHom φ φst) = Set.MapsTo.restrict (↑φ) s t φst

@[simp]

theorem SimpleGraph.induceHom_id {V : Type u} (G : SimpleGraph V) (s : Set V) : SimpleGraph.induceHom SimpleGraph.Hom.id (_ : Set.MapsTo id s s) = SimpleGraph.Hom.id

@[simp]

theorem SimpleGraph.induceHom_comp {V : Type u} {W : Type v} {X : Type w} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} {s : Set V} {t : Set W} {r : Set X} (φ : G →g G') (φst : Set.MapsTo (↑φ) s t) (ψ : G' →g G'') (ψtr : Set.MapsTo (↑ψ) t r) : SimpleGraph.Hom.comp (SimpleGraph.induceHom ψ ψtr) (SimpleGraph.induceHom φ φst) = SimpleGraph.induceHom (SimpleGraph.Hom.comp ψ φ) (_ : Set.MapsTo (↑ψ ∘ fun x => ↑φ x) s r)

theorem SimpleGraph.induceHom_injective {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G') (φst : Set.MapsTo (↑φ) s t) (hi : Set.InjOn (↑φ) s) : Function.Injective ↑(SimpleGraph.induceHom φ φst)

def SimpleGraph.induceHomOfLE {V : Type u} (G : SimpleGraph V) {s : Set V} {s' : Set V} (h : s ≤ s') : SimpleGraph.induce s G ↪g SimpleGraph.induce s' G

Given an inclusion of vertex subsets, the induced embedding on induced graphs. This is not an abbreviation for induceHom since we get an embedding in this case.

@[simp]

theorem SimpleGraph.induceHomOfLE_apply {V : Type u} (G : SimpleGraph V) {s : Set V} {s' : Set V} (h : s ≤ s') (v : ↑s) : ↑(SimpleGraph.induceHomOfLE G h) v = Set.inclusion h v

@[simp]

theorem SimpleGraph.induceHomOfLE_toHom {V : Type u} (G : SimpleGraph V) {s : Set V} {s' : Set V} (h : s ≤ s') : SimpleGraph.Embedding.toHom (SimpleGraph.induceHomOfLE G h) = SimpleGraph.induceHom SimpleGraph.Hom.id (_ : Set.MapsTo id s s')

@[inline, reducible]

abbrev SimpleGraph.Iso.refl {V : Type u} {G : SimpleGraph V} : G ≃g G

The identity isomorphism of a graph with itself.

@[inline, reducible]

abbrev SimpleGraph.Iso.toEmbedding {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') : G ↪g G'

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

@[inline, reducible]

abbrev SimpleGraph.Iso.toHom {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') : G →g G'

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

@[inline, reducible]

abbrev SimpleGraph.Iso.symm {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') : G' ≃g G

The inverse of a graph isomorphism.

theorem SimpleGraph.Iso.map_adj_iff {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {v : V} {w : V} : SimpleGraph.Adj G' (↑f v) (↑f w) ↔ SimpleGraph.Adj G v w

theorem SimpleGraph.Iso.map_mem_edgeSet_iff {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {e : Sym2 V} : Sym2.map (↑f) e ∈ SimpleGraph.edgeSet G' ↔ e ∈ SimpleGraph.edgeSet G

theorem SimpleGraph.Iso.apply_mem_neighborSet_iff {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {v : V} {w : V} : ↑f w ∈ SimpleGraph.neighborSet G' (↑f v) ↔ w ∈ SimpleGraph.neighborSet G v

@[simp]

theorem SimpleGraph.Iso.mapEdgeSet_apply {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (e : ↑(SimpleGraph.edgeSet G)) : ↑(SimpleGraph.Iso.mapEdgeSet f) e = SimpleGraph.Hom.mapEdgeSet (RelEmbedding.toRelHom (RelIso.toRelEmbedding f)) e

@[simp]

theorem SimpleGraph.Iso.mapEdgeSet_symm_apply {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (e : ↑(SimpleGraph.edgeSet G')) : ↑(SimpleGraph.Iso.mapEdgeSet f).symm e = SimpleGraph.Hom.mapEdgeSet (RelEmbedding.toRelHom (RelIso.toRelEmbedding (SimpleGraph.Iso.symm f))) e

def SimpleGraph.Iso.mapEdgeSet {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') : ↑(SimpleGraph.edgeSet G) ≃ ↑(SimpleGraph.edgeSet G')

An isomorphism of graphs induces an equivalence of edge sets.

@[simp]

theorem SimpleGraph.Iso.mapNeighborSet_symm_apply_coe {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V) (w : ↑(SimpleGraph.neighborSet G' (↑f v))) : ↑(↑(SimpleGraph.Iso.mapNeighborSet f v).symm w) = ↑(SimpleGraph.Iso.symm f) ↑w

@[simp]

theorem SimpleGraph.Iso.mapNeighborSet_apply_coe {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V) (w : ↑(SimpleGraph.neighborSet G v)) : ↑(↑(SimpleGraph.Iso.mapNeighborSet f v) w) = ↑f ↑w

def SimpleGraph.Iso.mapNeighborSet {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V) : ↑(SimpleGraph.neighborSet G v) ≃ ↑(SimpleGraph.neighborSet G' (↑f v))

A graph isomorphism induces an equivalence of neighbor sets.

theorem SimpleGraph.Iso.card_eq_of_iso {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} [Fintype V] [Fintype W] (f : G ≃g G') : Fintype.card V = Fintype.card W

def SimpleGraph.Iso.comap {V : Type u} {W : Type v} (f : V ≃ W) (G : SimpleGraph W) : SimpleGraph.comap (↑(Equiv.toEmbedding f)) G ≃g G

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

@[simp]

theorem SimpleGraph.Iso.comap_apply {V : Type u} {W : Type v} (f : V ≃ W) (G : SimpleGraph W) (v : V) : ↑(SimpleGraph.Iso.comap f G) v = ↑f v

@[simp]

theorem SimpleGraph.Iso.comap_symm_apply {V : Type u} {W : Type v} (f : V ≃ W) (G : SimpleGraph W) (w : W) : ↑(SimpleGraph.Iso.symm (SimpleGraph.Iso.comap f G)) w = ↑f.symm w

def SimpleGraph.Iso.map {V : Type u} {W : Type v} (f : V ≃ W) (G : SimpleGraph V) : G ≃g SimpleGraph.map (Equiv.toEmbedding f) G

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

@[simp]

theorem SimpleGraph.Iso.map_apply {V : Type u} {W : Type v} (f : V ≃ W) (G : SimpleGraph V) (v : V) : ↑(SimpleGraph.Iso.map f G) v = ↑f v

@[simp]

theorem SimpleGraph.Iso.map_symm_apply {V : Type u} {W : Type v} (f : V ≃ W) (G : SimpleGraph V) (w : W) : ↑(SimpleGraph.Iso.symm (SimpleGraph.Iso.map f G)) w = ↑f.symm w

def SimpleGraph.Iso.completeGraph {α : Type u_3} {β : Type u_4} (f : α ≃ β) : ⊤ ≃g ⊤

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

theorem SimpleGraph.Iso.toEmbedding_completeGraph {α : Type u_3} {β : Type u_4} (f : α ≃ β) : SimpleGraph.Iso.toEmbedding (SimpleGraph.Iso.completeGraph f) = SimpleGraph.Embedding.completeGraph (Equiv.toEmbedding f)

@[inline, reducible]

abbrev SimpleGraph.Iso.comp {V : Type u} {W : Type v} {X : Type w} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ≃g G'') (f : G ≃g G') : G ≃g G''

Composition of graph isomorphisms.

@[simp]

theorem SimpleGraph.Iso.coe_comp {V : Type u} {W : Type v} {X : Type w} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X} (f' : G' ≃g G'') (f : G ≃g G') : ↑(SimpleGraph.Iso.comp f' f) = ↑f' ∘ ↑f

@[simp]

theorem SimpleGraph.induceUnivIso_apply {V : Type u} (G : SimpleGraph V) (self : { x // x ∈ Set.univ }) : ↑(SimpleGraph.induceUnivIso G) self = ↑self

@[simp]

theorem SimpleGraph.induceUnivIso_symm_apply_coe {V : Type u} (G : SimpleGraph V) (a : V) : ↑(↑(RelIso.symm (SimpleGraph.induceUnivIso G)) a) = a

def SimpleGraph.induceUnivIso {V : Type u} (G : SimpleGraph V) : SimpleGraph.induce Set.univ G ≃g G

The graph induced on Set.univ is isomorphic to the original graph.