theorem finite_list_nodup (α : Type u_3) [Finite α] : {L : List α | L.Nodup}.Finite

@[simp]

theorem List.nodup_attachWith {α : Type u_3} {l : List α} (P : α → Prop) (hP : ∀ x ∈ l, P x) : (l.attachWith P hP).Nodup ↔ l.Nodup

Finiteness

class Graph.EdgeFinite {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

• edgeSet_finite : G.edgeSet.Finite

theorem Graph.edgeFinite_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.EdgeFinite ↔ G.edgeSet.Finite

theorem Graph.edgeFinite_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} [G.EdgeFinite] (hHG : H ≤ G) : H.EdgeFinite

instance Graph.instEdgeFiniteDeleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} [G.EdgeFinite] : (G.deleteVerts X).EdgeFinite

instance Graph.instEdgeFiniteRestrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} [G.EdgeFinite] : (G.restrict F).EdgeFinite

instance Graph.instEdgeFiniteDeleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} [G.EdgeFinite] : (G.deleteEdges F).EdgeFinite

theorem Graph.edgeFinite_induce {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} [G.EdgeFinite] (hX : X ⊆ G.vertexSet) : G[X].EdgeFinite

@[simp]

theorem Graph.edgeSet_finite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.EdgeFinite] : G.edgeSet.Finite

theorem Graph.incVertexSet_finite {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.EdgeFinite] (F : Set β) : V(G, F).Finite

theorem Graph.nonempty_isTrail_finite {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.EdgeFinite] : {P : WList α β | P.Nonempty ∧ G.IsTrail P}.Finite

theorem Graph.exists_le_maximal_isTrail {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.EdgeFinite] {t : WList α β} (ht : G.IsTrail t) : ∃ (m : WList α β), t ≤ m ∧ Maximal G.IsTrail m

theorem Graph.exists_le_maximal_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.EdgeFinite] {p : WList α β} (hp : G.IsPath p) : ∃ (m : WList α β), p ≤ m ∧ Maximal G.IsPath m

theorem Graph.exists_le_maximal_isCyclicWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} [G.EdgeFinite] (hC : G.IsCyclicWalk C) : ∃ (m : WList α β), C ≤ m ∧ Maximal G.IsCyclicWalk m

class Graph.Finite {α : Type u_1} {β : Type u_2} (G : Graph α β) extends G.EdgeFinite : Prop

A graph is finite if it has finitely many vertices and edges

• edgeSet_finite : G.edgeSet.Finite
• vertexSet_finite : G.vertexSet.Finite

theorem Graph.finite_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.Finite ↔ G.EdgeFinite ∧ G.vertexSet.Finite

theorem Graph.Finite.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.Finite) (hHG : H ≤ G) : H.Finite

theorem Graph.finite_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} [G.Finite] (hHG : H ≤ G) : H.Finite

instance Graph.instFiniteDeleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (X : Set α) : (G.deleteVerts X).Finite

instance Graph.instFiniteRestrict {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (F : Set β) : (G.restrict F).Finite

instance Graph.instFiniteDeleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (F : Set β) : (G.deleteEdges F).Finite

theorem Graph.Finite.induce {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} (hG : G.Finite) (hX : X ⊆ G.vertexSet) : G[X].Finite

@[simp]

theorem Graph.vertexSet_finite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] : G.vertexSet.Finite

theorem Graph.isTrail_finite {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : {P : WList α β | G.IsTrail P}.Finite

theorem Graph.isPath_finite {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : {P : WList α β | G.IsPath P}.Finite

theorem Graph.IsPath.vertex_length_le_ncard {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} [G.Finite] (hP : G.IsPath P) : P.vertex.length ≤ G.vertexSet.ncard

theorem Graph.IsPath.length_le_ncard {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} [G.Finite] (hP : G.IsPath P) : P.length + 1 ≤ G.vertexSet.ncard

theorem Graph.isCyclicWalk_finite {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : {C : WList α β | G.IsCyclicWalk C}.Finite

theorem Graph.finite_setOf_le {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : {H : Graph α β | H ≤ G}.Finite

A finite graph has finitely many subgraphs.

theorem Graph.finite_of_vertexSet_finite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Simple] (h : G.vertexSet.Finite) : G.Finite

@[simp]

theorem Graph.Simple.vertexSet_finite_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Simple] : G.vertexSet.Finite ↔ G.Finite

instance Graph.instFiniteSubgraphOfFinite {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : Finite G.Subgraph

instance Graph.instFiniteClosedSubgraphOfFinite {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : Finite G.ClosedSubgraph

instance Graph.instFiniteUnion {α : Type u_1} {β : Type u_2} {G H : Graph α β} [G.Finite] [H.Finite] : (G ∪ H).Finite

instance Graph.instEdgeFiniteNoEdge {α : Type u_1} {β : Type u_2} (V : Set α) : (noEdge V β).EdgeFinite

@[simp]

theorem Graph.noEdge_finite {α : Type u_1} {β : Type u_2} (V : Set α) : (noEdge V β).Finite ↔ V.Finite

instance Graph.instFiniteSingleEdge {α : Type u_1} {β : Type u_2} {x y : α} {e : β} : (Graph.singleEdge x y e).Finite

@[simp]

theorem Graph.banana_finite {α : Type u_1} {β : Type u_2} (u v : α) (F : Set β) : (banana u v F).Finite ↔ F.Finite

instance Graph.instFiniteToGraph {α : Type u_1} {β : Type u_2} (W : WList α β) : W.toGraph.Finite

theorem Graph.encard_delete_vertex_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] (hx : x ∈ G.vertexSet) : (G.deleteVerts {x}).vertexSet.encard < G.vertexSet.encard

Used for well-founded induction on finite graphs by number of vertices

theorem Graph.encard_delete_vertexSet_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} [G.Finite] (hX : (G.vertexSet ∩ X).Nonempty) : (G.deleteVerts X).vertexSet.encard < G.vertexSet.encard

theorem Graph.ncard_delete_vertex_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] (hx : x ∈ G.vertexSet) : (G.deleteVerts {x}).vertexSet.ncard < G.vertexSet.ncard

theorem Graph.ncard_delete_vertexSet_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} [G.Finite] (hX : (G.vertexSet ∩ X).Nonempty) : (G.deleteVerts X).vertexSet.ncard < G.vertexSet.ncard

theorem Graph.encard_delete_edge_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} [G.Finite] (he : e ∈ G.edgeSet) : (G.deleteEdges {e}).edgeSet.encard < G.edgeSet.encard

Used for well-founded induction on finite graphs by number of edges

theorem Graph.encard_delete_edgeSet_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} [G.Finite] (hF : (G.edgeSet ∩ F).Nonempty) : (G.deleteEdges F).edgeSet.encard < G.edgeSet.encard

theorem Graph.ncard_delete_edge_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} [G.Finite] (he : e ∈ G.edgeSet) : (G.deleteEdges {e}).edgeSet.ncard < G.edgeSet.ncard

theorem Graph.ncard_delete_edgeSet_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} [G.Finite] (hF : (G.edgeSet ∩ F).Nonempty) : (G.deleteEdges F).edgeSet.ncard < G.edgeSet.ncard

theorem Graph.of_not_exists_minimal {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : Graph α β → Prop} [G.Finite] (h : ∀ H ≤ G, H.Finite → ¬Minimal (fun (x : Graph α β) => ¬P x) H) : P G

Local Finiteness

class Graph.LocallyFinite {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

A graph is LocallyFinite if each of its vertices is incident with finitely many edges.

• finite (x : α) : E(G, x).Finite

theorem Graph.locallyFinite_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.LocallyFinite ↔ ∀ (x : α), E(G, x).Finite

theorem Graph.finite_incEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.LocallyFinite] (x : α) : E(G, x).Finite

theorem Graph.finite_neighbors {α : Type u_1} {β : Type u_2} {x : α} (G : Graph α β) [G.LocallyFinite] : N(G, x).Finite

theorem Graph.finite_setOf_isNonloopAt {α : Type u_1} {β : Type u_2} {x : α} (G : Graph α β) [G.LocallyFinite] : {e : β | G.IsNonloopAt e x}.Finite

theorem Graph.finite_setOf_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} (G : Graph α β) [G.LocallyFinite] : {e : β | G.IsLoopAt e x}.Finite

instance Graph.instLocallyFiniteOfFinite {α : Type u_1} {β : Type u_2} [Finite β] (G : Graph α β) : G.LocallyFinite

theorem Graph.LocallyFinite.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.LocallyFinite) (hle : H ≤ G) : H.LocallyFinite

instance Graph.instLocallyFiniteInduce {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.LocallyFinite] (X : Set α) : G[X].LocallyFinite

instance Graph.instLocallyFiniteDeleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.LocallyFinite] (X : Set α) : (G.deleteVerts X).LocallyFinite

instance Graph.instLocallyFiniteRestrict {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.LocallyFinite] (F : Set β) : (G.restrict F).LocallyFinite

instance Graph.instLocallyFiniteDeleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.LocallyFinite] (F : Set β) : (G.deleteEdges F).LocallyFinite

instance Graph.instLocallyFiniteOfEdgeFinite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.EdgeFinite] : G.LocallyFinite

instance Graph.instLocallyFiniteUnion {α : Type u_1} {β : Type u_2} {G H : Graph α β} [G.LocallyFinite] [H.LocallyFinite] : (G ∪ H).LocallyFinite

instance Graph.instLocallyFiniteNoEdge {α : Type u_1} {β : Type u_2} (V : Set α) : (noEdge V β).LocallyFinite

@[simp]

theorem Graph.vertexSet_finite_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.LocallyFinite] : G.vertexSet.Finite ↔ G.Finite

instance Graph.completeBipartiteGraph_finite (m n : ℕ) : (CompleteBipartiteGraph m n).Finite

instance Graph.completeGraph_finite (n : ℕ) : (CompleteGraph n).Finite