def Graph.IsCycleSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (C : Set β) : Prop

G.IsCycleSet C means that C is the edge set of a cycle of G.

Equations

• G.IsCycleSet C = ∃ (C₀ : WList α β), G.IsCyclicWalk C₀ ∧ C₀.edgeSet = C

theorem Graph.IsCyclicWalk.isCycleSet_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : G.IsCycleSet C.edgeSet

theorem Graph.isCycleSet_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {C' : Set β} : G.IsCycleSet C' ↔ ∃ C ≤ G, C.IsCycle ∧ C' = C.edgeSet

@[simp]

theorem Graph.restrict_isCycleSet_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (C : Set β) : (G.restrict F).IsCycleSet C ↔ G.IsCycleSet C ∧ C ⊆ F

@[simp]

theorem Graph.deleteEdges_isCycleSet_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (C : Set β) : (G.deleteEdges F).IsCycleSet C ↔ G.IsCycleSet C ∧ Disjoint C F

@[simp]

theorem Graph.induce_isCycleSet_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} (C : Set β) : G[X].IsCycleSet C ↔ ∃ (C₀ : WList α β), G.IsCyclicWalk C₀ ∧ C₀.vertexSet ⊆ X ∧ C₀.edgeSet = C

@[simp]

theorem Graph.deleteVerts_isCycleSet_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} (C : Set β) : (G.deleteVerts X).IsCycleSet C ↔ ∃ (C₀ : WList α β), G.IsCyclicWalk C₀ ∧ Disjoint C₀.vertexSet X ∧ C₀.edgeSet = C

theorem Graph.IsCycleSet.of_isLink {α : Type u_1} {β : Type u_2} {G H : Graph α β} {C : Set β} (h : G.IsCycleSet C) (he : ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → H.IsLink e x y) : H.IsCycleSet C

theorem Graph.IsClosedSubgraph.isCycleSet {α : Type u_1} {β : Type u_2} {G H : Graph α β} {C : Set β} (hC : G.IsCycleSet C) (hHG : H.IsClosedSubgraph G) : H.IsCycleSet C ∨ (G.deleteVerts H.vertexSet).IsCycleSet C

theorem Graph.IsLoopAt.isCycleSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {e : β} (h : G.IsLoopAt e x) : G.IsCycleSet {e}

theorem Graph.isCycleSet_singleton_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} : G.IsCycleSet {e} ↔ ∃ (x : α), G.IsLoopAt e x

theorem Graph.isCycleSet_pair_iff_parallel {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] {e f : β} (hef : e ≠ f) : G.IsCycleSet {e, f} ↔ G.parallel e f

def Graph.IsAcyclicSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (I : Set β) : Prop

G.IsAcyclicSet X means that the subgraph G ↾ X is a forest.

Equations

• G.IsAcyclicSet I = (I ⊆ G.edgeSet ∧ ∀ (C₀ : WList α β), G.IsCyclicWalk C₀ → ¬C₀.edgeSet ⊆ I)

theorem Graph.restrict_isForest_iff' {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} : (G.restrict F).IsForest ↔ ∀ (C : WList α β), C.edgeSet ⊆ F → ¬G.IsCyclicWalk C

theorem Graph.restrict_isForest_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : F ⊆ G.edgeSet) : (G.restrict F).IsForest ↔ G.IsAcyclicSet F

theorem Graph.isAcyclicSet_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} : G.IsAcyclicSet F ↔ F ⊆ G.edgeSet ∧ (G.restrict F).IsForest

theorem Graph.not_isAcyclicSet_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : F ⊆ G.edgeSet) : ¬G.IsAcyclicSet F ↔ ∃ (C : Graph α β), C.IsCycle ∧ C ≤ G ∧ C.edgeSet ⊆ F

theorem Graph.IsAcyclicSet.subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : G.IsAcyclicSet F) : F ⊆ G.edgeSet

theorem Graph.IsAcyclicSet.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (hGH : G ≤ H) (hF : G.IsAcyclicSet F) : H.IsAcyclicSet F

theorem Graph.IsAcyclicSet.anti_inter {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (hGH : G ≤ H) (hF : H.IsAcyclicSet F) : G.IsAcyclicSet (G.edgeSet ∩ F)

theorem Graph.IsAcyclicSet.anti {α : Type u_1} {β : Type u_2} {G : Graph α β} {F F' : Set β} (hsu : F' ⊆ F) (hF : G.IsAcyclicSet F) : G.IsAcyclicSet F'

theorem Graph.IsAcyclicSet.isBridge {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {F : Set β} (hF : G.IsAcyclicSet F) (he : e ∈ F) : (G.restrict F).IsBridge e

theorem Graph.IsAcyclicSet.of_deleteEdges_isBond {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {F B : Set β} (hB : G.IsBond B) (hF : (G.deleteEdges B).IsAcyclicSet F) (he : e ∈ B) : G.IsAcyclicSet (insert e F)

theorem Graph.IsClosedSubgraph.isAcyclicSet_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} {I J : Set β} (hI : G.IsAcyclicSet I) (hJ : G.IsAcyclicSet J) (hIH : I ⊆ H.edgeSet) (hJH : J ⊆ G.edgeSet \ H.edgeSet) (h : H.IsClosedSubgraph G) : G.IsAcyclicSet (I ∪ J)

def Graph.IsMaximalAcyclicSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : Prop

Equations

• G.IsMaximalAcyclicSet F = Maximal G.IsAcyclicSet F

theorem Graph.IsMaximalAcyclicSet.isAcyclicSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : G.IsMaximalAcyclicSet F) : G.IsAcyclicSet F

@[simp]

theorem Graph.IsMaximalAcyclicSet.subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : G.IsMaximalAcyclicSet F) : F ⊆ G.edgeSet

theorem Graph.IsMaximalAcyclicSet.insert_not_isBridge {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {F : Set β} (he : e ∈ G.edgeSet \ F) (hF : G.IsMaximalAcyclicSet F) : ¬(G.restrict (insert e F)).IsBridge e

theorem Graph.IsMaximalAcyclicSet.connBetween_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {F : Set β} (hF : G.IsMaximalAcyclicSet F) : (G.restrict F).ConnBetween x y ↔ G.ConnBetween x y