Documentation

🔹 coverage

def SimpleGraph.IsAcyclic {V : Type u_1} (G : SimpleGraph V) :

Prop

A graph is acyclic (or a forest) if it has no cycles.

Instances For

🔶 coverage

structure SimpleGraph.IsTree {V : Type u_1} (G : SimpleGraph V) extends G.Connected :

Prop

A tree is a connected acyclic graph.

preconnected : G.Preconnected
nonempty : Nonempty V
isAcyclic : G.IsAcyclic
A tree is acyclic.

Instances For

theorem SimpleGraph.isTree_iff {V : Type u_1} (G : SimpleGraph V) :

G.IsTree ↔ G.Connected ∧ G.IsAcyclic

@[deprecated SimpleGraph.IsTree.connected (since := "2026-03-18")]

theorem SimpleGraph.IsTree.isConnected {V : Type u_1} {G : SimpleGraph V} (self : G.IsTree) :

G.Connected

Alias of SimpleGraph.IsTree.connected.

@[deprecated SimpleGraph.IsTree.isAcyclic (since := "2026-03-18")]

theorem SimpleGraph.IsTree.IsAcyclic {V : Type u_1} {G : SimpleGraph V} (self : G.IsTree) :

Alias of SimpleGraph.IsTree.isAcyclic.

A tree is acyclic.

@[simp]

theorem SimpleGraph.isAcyclic_bot {V : Type u_1} :

⊥.IsAcyclic

theorem SimpleGraph.IsAcyclic.comap {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective ⇑f) (h : G'.IsAcyclic) :

A graph that has an injective homomorphism to an acyclic graph is acyclic.

theorem SimpleGraph.IsAcyclic.embedding {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') (h : G'.IsAcyclic) :

theorem SimpleGraph.Iso.isAcyclic_iff {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ≃g G') :

G.IsAcyclic ↔ G'.IsAcyclic

Isomorphic graphs are acyclic together.

theorem SimpleGraph.Iso.isTree_iff {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ≃g G') :

G.IsTree ↔ G'.IsTree

Isomorphic graphs are trees together.

theorem SimpleGraph.IsAcyclic.of_map {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} (f : V ↪ V') (h : (SimpleGraph.map (⇑f) G).IsAcyclic) :

theorem SimpleGraph.IsAcyclic.of_comap {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} (f : V' ↪ V) (h : G.IsAcyclic) :

(SimpleGraph.comap (⇑f) G).IsAcyclic

theorem SimpleGraph.IsAcyclic.induce {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) (s : Set V) :

(SimpleGraph.induce s G).IsAcyclic

A graph induced from an acyclic graph is acyclic.

theorem SimpleGraph.IsAcyclic.subgraph {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) (H : G.Subgraph) :

H.coe.IsAcyclic

A subgraph of an acyclic graph is acyclic.

theorem SimpleGraph.IsAcyclic.anti {V : Type u_1} {G G' : SimpleGraph V} (hsub : G ≤ G') (h : G'.IsAcyclic) :

A spanning subgraph of an acyclic graph is acyclic.

theorem SimpleGraph.isAcyclic_sSup_of_isAcyclic_directedOn {V : Type u_1} (Hs : Set (SimpleGraph V)) (h_acyc : ∀ H ∈ Hs, H.IsAcyclic) (h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) => x1 ≤ x2) Hs) :

(sSup Hs).IsAcyclic

The directed supremum of acyclic graphs is acylic.

theorem SimpleGraph.exists_maximal_isAcyclic_of_le_isAcyclic {V : Type u_1} {G H : SimpleGraph V} (hHG : H ≤ G) (hH : H.IsAcyclic) :

∃ (H' : SimpleGraph V), H ≤ H' ∧ Maximal (fun (H : SimpleGraph V) => H ≤ G ∧ H.IsAcyclic) H'

Every acyclic subgraph H ≤ G is contained in a maximal such subgraph.

theorem SimpleGraph.IsAcyclic.isTree_connectedComponent {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) (c : G.ConnectedComponent) :

c.toSimpleGraph.IsTree

A connected component of an acyclic graph is a tree.

theorem SimpleGraph.IsAcyclic.of_card_le_two {V : Type u_1} {G : SimpleGraph V} (h : ENat.card V ≤ 2) :

theorem SimpleGraph.IsAcyclic.of_subsingleton {V : Type u_1} [Subsingleton V] {G : SimpleGraph V} :

theorem SimpleGraph.Subgraph.isAcyclic_coe_bot {V : Type u_1} (G : SimpleGraph V) :

⊥.coe.IsAcyclic

theorem SimpleGraph.IsTree.of_subsingleton {V : Type u_1} [Nonempty V] [Subsingleton V] {G : SimpleGraph V} :

G.IsTree

theorem SimpleGraph.IsTree.coe_singletonSubgraph {V : Type u_1} (G : SimpleGraph V) (v : V) :

(G.singletonSubgraph v).coe.IsTree

theorem SimpleGraph.IsTree.coe_subgraphOfAdj {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) :

(G.subgraphOfAdj h).coe.IsTree

theorem SimpleGraph.isAcyclic_iff_forall_adj_isBridge {V : Type u_1} {G : SimpleGraph V} :

G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)

theorem SimpleGraph.isAcyclic_iff_forall_edge_isBridge {V : Type u_1} {G : SimpleGraph V} :

G.IsAcyclic ↔ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e

theorem SimpleGraph.IsAcyclic.path_unique {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) {v w : V} (p q : G.Path v w) :

p = q

theorem SimpleGraph.isAcyclic_of_path_unique {V : Type u_1} {G : SimpleGraph V} (h : ∀ (v w : V) (p q : G.Path v w), p = q) :

theorem SimpleGraph.isAcyclic_iff_path_unique {V : Type u_1} {G : SimpleGraph V} :

G.IsAcyclic ↔ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q

theorem SimpleGraph.IsAcyclic.mem_support_of_ne_mem_support_of_adj_of_isPath {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} {p : G.Walk u v} {q : G.Walk u w} (hp : p.IsPath) (hq : q.IsPath) (hadj : G.Adj v w) (hv : v ∉ q.support) :

w ∈ p.support

theorem SimpleGraph.IsAcyclic.ne_mem_support_of_support_of_adj_of_isPath {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} {p : G.Walk u v} {q : G.Walk u w} (hp : p.IsPath) (hq : q.IsPath) (hadj : G.Adj v w) (hw : w ∈ p.support) :

v ∉ q.support

theorem SimpleGraph.IsAcyclic.path_concat {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} {p : G.Walk u v} {q : G.Walk u w} (hp : p.IsPath) (hq : q.IsPath) (hadj : G.Adj v w) (hv : v ∈ q.support) :

q = p.concat hadj

theorem SimpleGraph.isTree_iff_existsUnique_path {V : Type u_1} {G : SimpleGraph V} :

G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath

theorem SimpleGraph.IsTree.existsUnique_path {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (v w : V) :

∃! p : G.Walk v w, p.IsPath

theorem SimpleGraph.IsAcyclic.isPath_iff_isChain {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) :

p.IsPath ↔ List.IsChain (fun (x1 x2 : Sym2 V) => x1 ≠ x2) p.edges

theorem SimpleGraph.IsAcyclic.isPath_iff_isTrail {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) :

p.IsPath ↔ p.IsTrail

theorem SimpleGraph.IsTree.card_edgeFinset {V : Type u_1} {G : SimpleGraph V} [Fintype V] [Fintype ↑G.edgeSet] (hG : G.IsTree) :

G.edgeFinset.card + 1 = Fintype.card V

theorem SimpleGraph.isTree_of_minimal_connected {V : Type u_1} {G : SimpleGraph V} (h : Minimal Connected G) :

G.IsTree

A minimally connected graph is a tree.

theorem SimpleGraph.isTree_iff_minimal_connected {V : Type u_1} {G : SimpleGraph V} :

G.IsTree ↔ Minimal Connected G

theorem SimpleGraph.IsAcyclic.isAcyclic_sup_fromEdgeSet_of_not_reachable {V : Type u_1} {G : SimpleGraph V} {u v : V} (hnreach : ¬G.Reachable u v) (hacyc : G.IsAcyclic) :

(G ⊔ fromEdgeSet {s(u, v)}).IsAcyclic

Connecting two unreachable vertices by an edge preserves acyclicity.

theorem SimpleGraph.isAcyclic_add_edge_iff_of_not_reachable {V : Type u_1} {G : SimpleGraph V} (x y : V) (hxy : ¬G.Reachable x y) :

(G ⊔ fromEdgeSet {s(x, y)}).IsAcyclic ↔ G.IsAcyclic

theorem SimpleGraph.isAcyclic_sup_fromEdgeSet_iff {V : Type u_1} {G : SimpleGraph V} {u v : V} :

(G ⊔ fromEdgeSet {s(u, v)}).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)

Adding an edge results in an acyclic graph iff the original graph was acyclic and the edge connects vertices that previously had no path between them.

theorem SimpleGraph.reachable_eq_of_maximal_isAcyclic {V : Type u_1} {G : SimpleGraph V} (F : SimpleGraph V) (h : Maximal (fun (H : SimpleGraph V) => H ≤ G ∧ H.IsAcyclic) F) :

F.Reachable = G.Reachable

The reachability relation of a maximal acyclic subgraph agrees with that of the larger graph.

theorem SimpleGraph.maximal_isAcyclic_iff_reachable_eq {V : Type u_1} {G F : SimpleGraph V} (hle : F ≤ G) (hF : F.IsAcyclic) :

Maximal (fun (F : SimpleGraph V) => F ≤ G ∧ F.IsAcyclic) F ↔ F.Reachable = G.Reachable

A subgraph is maximal acyclic iff its reachability relation agrees with the larger graph.

theorem SimpleGraph.Connected.maximal_le_isAcyclic_iff_isTree {V : Type u_1} {G T : SimpleGraph V} (hG : G.Connected) (hT : T ≤ G) :

Maximal (fun (H : SimpleGraph V) => H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree

A subgraph of a connected graph is maximal acyclic iff it is a tree.

@[simp]

theorem SimpleGraph.maximal_isAcyclic_iff_isTree {V : Type u_1} [Nonempty V] {T : SimpleGraph V} :

Maximal IsAcyclic T ↔ T.IsTree

theorem SimpleGraph.isTree_iff_maximal_isAcyclic {V : Type u_1} {G : SimpleGraph V} :

G.IsTree ↔ Nonempty V ∧ Maximal IsAcyclic G

A maximally acyclic graph is a tree. This is similar to maximal_isAcyclic_iff_isTree except with Nonempty V as part of the iff rather than an assumption.

theorem SimpleGraph.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic {V : Type u_1} {G H : SimpleGraph V} (hH_le : H ≤ G) (hH_isAcyclic : H.IsAcyclic) :

∃ (F : SimpleGraph V), H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable

Every acyclic subgraph can be extended to a spanning forest.

theorem SimpleGraph.exists_isAcyclic_reachable_eq_le {V : Type u_1} {G : SimpleGraph V} :

∃ F ≤ G, F.IsAcyclic ∧ F.Reachable = G.Reachable

Every graph has a spanning forest.

theorem SimpleGraph.Connected.exists_isTree_le_of_le_of_isAcyclic {V : Type u_1} {G H : SimpleGraph V} (h : G.Connected) (hH_le : H ≤ G) (hH_isAcyclic : H.IsAcyclic) :

∃ (F : SimpleGraph V), H ≤ F ∧ F ≤ G ∧ F.IsTree

Every acyclic subgraph of a connected graph can be extended to a spanning tree.

theorem SimpleGraph.Connected.exists_isTree_le {V : Type u_1} {G : SimpleGraph V} (h : G.Connected) :

∃ T ≤ G, T.IsTree

Every connected graph has a spanning tree.

theorem SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one {V : Type u_1} {G : SimpleGraph V} (h : G.Connected) :

Nat.card V ≤ Nat.card ↑G.edgeSet + 1

Every connected graph on n vertices has at least n-1 edges.

theorem SimpleGraph.isTree_iff_connected_and_card {V : Type u_1} {G : SimpleGraph V} [Finite V] :

G.IsTree ↔ G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V

theorem SimpleGraph.IsTree.minDegree_eq_one_of_nontrivial {V : Type u_1} {G : SimpleGraph V} (h : G.IsTree) [Fintype V] [Nontrivial V] [DecidableRel G.Adj] :

G.minDegree = 1

The minimum degree of all vertices in a nontrivial tree is one.

theorem SimpleGraph.IsTree.exists_vert_degree_one_of_nontrivial {V : Type u_1} {G : SimpleGraph V} [Fintype V] [Nontrivial V] [DecidableRel G.Adj] (h : G.IsTree) :

∃ (v : V), G.degree v = 1

A nontrivial tree has a vertex of degree one.

theorem SimpleGraph.Connected.induce_compl_singleton_of_degree_eq_one {V : Type u_1} {G : SimpleGraph V} (hconn : G.Connected) {v : V} [Fintype ↑(G.neighborSet v)] (hdeg : G.degree v = 1) :

(induce {v}ᶜ G).Connected

The graph resulting from removing a vertex of degree one from a connected graph is connected.

theorem SimpleGraph.Connected.exists_connected_induce_compl_singleton_of_finite_nontrivial {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nontrivial V] (hconn : G.Connected) :

∃ (v : V), (induce {v}ᶜ G).Connected

A finite nontrivial connected graph contains a vertex that leaves the graph connected if removed.

theorem SimpleGraph.Connected.exists_preconnected_induce_compl_singleton_of_finite {V : Type u_1} {G : SimpleGraph V} [Finite V] (hconn : G.Connected) :

∃ (v : V), (induce {v}ᶜ G).Preconnected

A finite connected graph contains a vertex that leaves the graph preconnected if removed.

theorem SimpleGraph.IsAcyclic.dist_ne_of_adj {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} (hadj : G.Adj v w) (hreach : G.Reachable u v) :

G.dist u v ≠ G.dist u w

theorem SimpleGraph.IsTree.dist_ne_of_adj {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (u : V) {v w : V} (hadj : G.Adj v w) :

G.dist u v ≠ G.dist u w

theorem SimpleGraph.IsAcyclic.dist_eq_dist_add_one_of_adj_of_reachable {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) (u : V) {v w : V} (hadj : G.Adj v w) (hreach : G.Reachable u v) :

G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1

theorem SimpleGraph.IsTree.dist_eq_dist_add_one_of_adj {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (u : V) {v w : V} (hadj : G.Adj v w) :

G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1

noncomputable def SimpleGraph.IsTree.coloringTwoOfVert {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (u : V) :

G.Coloring (Fin 2)

The unique two-coloring of a tree that colors the given vertex with zero

Instances For

noncomputable def SimpleGraph.IsTree.coloringTwo {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) :

G.Coloring (Fin 2)

Arbitrary coloring with two colors for a tree

Instances For

theorem SimpleGraph.IsTree.isBipartite {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) :

G.IsBipartite

noncomputable def SimpleGraph.IsAcyclic.coloringTwoOfVerts {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) (verts : G.ConnectedComponent → V) (h : ∀ (C : G.ConnectedComponent), verts C ∈ C) :

G.Coloring (Fin 2)

The unique two-coloring of a forest that colors the given vertices with zero

Instances For

noncomputable def SimpleGraph.IsAcyclic.coloringTwo {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) :

G.Coloring (Fin 2)

Arbitrary coloring with two colors for a forest

Instances For

theorem SimpleGraph.IsAcyclic.isBipartite {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) :

G.IsBipartite

theorem SimpleGraph.IsAcyclic.colorable_two {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) :

G.Colorable 2

An acyclic graph (forest) is 2-colorable.

theorem SimpleGraph.IsTree.colorable_two {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) :

G.Colorable 2

A tree is 2-colorable.

theorem SimpleGraph.IsAcyclic.chromaticNumber_le_two {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) :

G.chromaticNumber ≤ 2

The chromatic number of an acyclic graph (forest) is at most 2.

theorem SimpleGraph.IsTree.chromaticNumber_le_two {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) :

G.chromaticNumber ≤ 2

The chromatic number of a tree is at most 2.

theorem SimpleGraph.exists_isCycle_of_two_le_isEdgeReachable {V : Type u_1} {G : SimpleGraph V} {u v : V} (huv : u ≠ v) {n : ℕ} (hn : 2 ≤ n) (h : G.IsEdgeReachable n u v) :

∃ (w : G.Walk u u), w.IsCycle