def Graph.cycleMatroid {α : Type u_1} {β : Type u_2} (G : Graph α β) : Matroid β

The cycle matroid of a graph G. Its circuits are the edge sets of cycles of G, and its independent sets are the edge sets of forests.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Graph.cycleMatroid_E {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.cycleMatroid.E = G.edgeSet

instance Graph.instFinitaryCycleMatroid {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.cycleMatroid.Finitary

@[simp]

theorem Graph.cycleMatroid_isCircuit {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.cycleMatroid.IsCircuit = G.IsCycleSet

@[simp]

theorem Graph.cycleMatroid_indep {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.cycleMatroid.Indep = G.IsAcyclicSet

theorem Graph.cycleMatroid_isBase {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.cycleMatroid.IsBase = G.IsMaximalAcyclicSet

theorem Graph.isBase_iff_indep_spanning {α : Type u_1} {M : Matroid α} {X : Set α} : M.IsBase X ↔ M.Indep X ∧ M.Spanning X

theorem Graph.exists_isMaximalAcyclicSet {α : Type u_1} {β : Type u_2} (G : Graph α β) : ∃ (F : Set β), G.IsMaximalAcyclicSet F

theorem Graph.cycleMatroid_coindep {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} : G.cycleMatroid.Coindep F ↔ F ⊆ G.edgeSet ∧ ∀ (x y : α), G.ConnBetween x y ↔ (G.deleteEdges F).ConnBetween x y

theorem Graph.cycleMatroid_spanning {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} : G.cycleMatroid.Spanning F ↔ F ⊆ G.edgeSet ∧ ∀ (x y : α), G.ConnBetween x y ↔ (G.restrict F).ConnBetween x y

@[simp]

theorem Graph.cycleMatroid_cocircuit {α : Type u_1} {β : Type u_2} (G : Graph α β) (C : Set β) : G.cycleMatroid.IsCocircuit C ↔ G.IsBond C

@[simp]

theorem Graph.cycleMatroid_coloop {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : G.cycleMatroid.IsColoop e ↔ G.IsBridge e

theorem Graph.IsEdgeCut.cycleMatroid_dual_cyclic {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : G.IsEdgeCut F) : G.cycleMatroid✶.Cyclic F

theorem Graph.IsMaximalAcyclicSet.isTree {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hG : G.Connected) (hF : G.IsMaximalAcyclicSet F) : (G.restrict F).IsTree

@[simp]

theorem Graph.cycleMatroid_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : (G.restrict F).cycleMatroid = G.cycleMatroid.restrict (G.edgeSet ∩ F)

theorem Graph.restrict_cycleMatroid {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : F ⊆ G.edgeSet) : G.cycleMatroid.restrict F = (G.restrict F).cycleMatroid

@[simp]

theorem Graph.cycleMatroid_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : (G.deleteEdges F).cycleMatroid = G.cycleMatroid.delete F

theorem Graph.cycleMatroid_contract {α : Type u_1} {β : Type u_2} {G H : Graph α β} {φ : α → α} (hφ : H.connPartition.IsRepFun φ) (hHG : H ≤ G) : G /[H.edgeSet, φ].cycleMatroid = G.cycleMatroid.contract H.edgeSet

@[simp]

theorem Graph.cycleMatroid_deleteVerts_isolatedSet {α : Type u_1} {β : Type u_2} (G : Graph α β) : (G.deleteVerts G.IsolatedSet).cycleMatroid = G.cycleMatroid

theorem Graph.cycleMatroid_isRestriction_of_isLink {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hl : ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → H.IsLink e x y) : G.cycleMatroid.IsRestriction H.cycleMatroid

theorem Graph.cycleMatroid_isRestriction_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G ≤ H) : G.cycleMatroid.IsRestriction H.cycleMatroid

theorem Graph.cycleMatroid_isBasis {α : Type u_1} {β : Type u_2} {G : Graph α β} {B F : Set β} : G.cycleMatroid.IsBasis B F ↔ F ⊆ G.edgeSet ∧ (G.restrict F).IsMaximalAcyclicSet B

theorem Graph.Connected.eRk_cycleMatroid_restrict_add_one {α : Type u_1} {β : Type u_2} {G : Graph α β} {R : Set β} (hG : (G.restrict R).Connected) : G.cycleMatroid.eRk R + 1 = G.vertexSet.encard

theorem Graph.Connected.eRank_cycleMatroid_add_one {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Connected) : G.cycleMatroid.eRank + 1 = G.vertexSet.encard

theorem Graph.Preconnected.cycleMatroid_dual_girth {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Preconnected) (n : ℕ) : ↑n ≤ G.cycleMatroid✶.girth ↔ G.EdgeConnGE n

theorem Graph.cycleMatroid_loops {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.cycleMatroid.loops = ⋃ (x : α), loopSet x

theorem Graph.cycleMatroid_loopless_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.cycleMatroid.Loopless ↔ G.Loopless

instance Graph.instLooplessCycleMatroidOfLoopless {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] : G.cycleMatroid.Loopless

@[simp]

theorem Graph.cycleMatroid_isLoop {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : G.cycleMatroid.IsLoop e ↔ ∃ (v : α), G.IsLoopAt e v

theorem Graph.IsClosedSubgraph.cycleMatroid_skew {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsClosedSubgraph G) : G.cycleMatroid.Skew H.edgeSet (G.edgeSet \ H.edgeSet)

theorem Graph.Compatible.cycleMatroid_union_skew {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : (G.vertexSet ∩ H.vertexSet).Subsingleton) (hcompat : G.Compatible H) : (G ∪ H).cycleMatroid.Skew G.edgeSet H.edgeSet

theorem Graph.cycleMatroid_disjointSum {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : (G.vertexSet ∩ H.vertexSet).Subsingleton) (hdj : Disjoint G.edgeSet H.edgeSet) : (G ∪ H).cycleMatroid = G.cycleMatroid.disjointSum H.cycleMatroid hdj

theorem Graph.components_cycleMatroid_isSkewFamily {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.cycleMatroid.IsSkewFamily fun (H : ↑G.Components) => (↑H).edgeSet

theorem Graph.eRank_cycleMatroid_add_numberOfComponents {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.cycleMatroid.eRank + c(G) = G.vertexSet.encard

def Graph.joinAtMap {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) (f : α → α) [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] (y : α) : α

Vertex map used in Graph.joinAt.

Equations

• G.joinAtMap x f y = if y ∈ f '' G.vertexSet then x else y

theorem Graph.exists_joinAtMap_of_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] (hf : G.connPartition.IsRepFun f) (x : α) (hV : G.vertexSet.Nonempty) : ∃ y ∈ G.vertexSet, G.joinAtMap x f y = x

theorem Graph.joinAtMap_eq_of_joinAtMap_eq_joinAtMap {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] {y₁ y₂ : α} (h : G.joinAtMap x f y₁ = G.joinAtMap x f y₂) (hne : y₁ ≠ y₂) : G.joinAtMap x f y₁ = x

def Graph.joinAt {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) (f : α → α) [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] : Graph α β

Join the connected components of G at x using the function f. Has sound output when f is a rep-function of G.connPartition.

Equations

• G.joinAt x f = Graph.map (G.joinAtMap x f) G

@[simp]

theorem Graph.vertexSet_joinAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] (hf : G.connPartition.IsRepFun f) (hV : G.vertexSet.Nonempty) : (G.joinAt x f).vertexSet = insert x (G.vertexSet \ f '' G.vertexSet)

@[simp]

theorem Graph.edgeSet_joinAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] : (G.joinAt x f).edgeSet = G.edgeSet

theorem Graph.joinAt_finite {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] (hf : G.connPartition.IsRepFun f) [G.EdgeFinite] : (G.joinAt x f).Finite

theorem Graph.mem_vertexSet_joinAt_of_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] (hV : G.vertexSet.Nonempty) (hf : G.connPartition.IsRepFun f) : x ∈ (G.joinAt x f).vertexSet

theorem Graph.joinAt_preconnected {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] (hf : G.connPartition.IsRepFun f) : (G.joinAt x f).Preconnected

theorem Graph.IsWalk.of_joinAt_of_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] {W : WList α β} (hW : G.IsWalk W) (hfW : Disjoint W.vertexSet (f '' G.vertexSet)) : (G.joinAt v f).IsWalk W

theorem Graph.IsWalk.joinAt_of_notMem {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] {W : WList α β} (hW : (G.joinAt v f).IsWalk W) (hvW : v ∉ W) : G.IsWalk W

theorem Graph.IsCompOf.joinAtMap_injOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {f : α → α} {H : Graph α β} (hH : H.IsCompOf G) (hf : G.connPartition.IsRepFun f) (hx : x ∉ G.vertexSet \ f '' G.vertexSet) [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] : Set.InjOn (G.joinAtMap x f) H.vertexSet

theorem Graph.IsCycleSet.joinAt_of {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] {C : Set β} (hf : G.connPartition.IsRepFun f) (hx : x ∉ G.vertexSet \ f '' G.vertexSet) (hC : G.IsCycleSet C) : (G.joinAt x f).IsCycleSet C

theorem Graph.IsCycleSet.of_joinAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] {C : Set β} (hf : G.connPartition.IsRepFun f) (hx : x ∉ G.vertexSet \ f '' G.vertexSet) (hC : (G.joinAt x f).IsCycleSet C) : G.IsCycleSet C

@[simp]

theorem Graph.cycleMatroid_joinAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {f : α → α} [DecidablePred fun (x : α) => x ∈ f '' G.vertexSet] (hf : G.connPartition.IsRepFun f) (hx : x ∉ G.vertexSet \ f '' G.vertexSet) : (G.joinAt x f).cycleMatroid = G.cycleMatroid

@[simp]

theorem Graph.isNonloop_iff_of_loopless {β : Type u_2} {e : β} {M : Matroid β} [M.Loopless] : M.IsNonloop e ↔ e ∈ M.E

@[simp]

theorem Graph.cycleMatroid_parallel {α : Type u_1} {β : Type u_2} {G : Graph α β} {e f : β} [G.Loopless] : G.cycleMatroid.Parallel e f ↔ G.parallel e f

theorem Graph.cycleMatroid_parallelClasses {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] : G.cycleMatroid.parallelClasses = G.parallelClasses

@[simp]

theorem Graph.cycleMatroid_simple {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.cycleMatroid.Simple ↔ G.Simple

instance Graph.instSimpleCycleMatroidOfSimple {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Simple] : G.cycleMatroid.Simple

@[simp]

theorem Graph.cycleMatroid_finite {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.cycleMatroid.Finite ↔ G.EdgeFinite

instance Graph.instFiniteCycleMatroidOfEdgeFinite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.EdgeFinite] : G.cycleMatroid.Finite

@[simp]

theorem Graph.cycleMatroid_bot {α : Type u_1} {β : Type u_2} : ⊥.cycleMatroid = Matroid.emptyOn β

@[simp]

theorem Graph.cycleMatroid_noEdge {α : Type u_1} {β : Type u_2} {V : Set α} : (noEdge V β).cycleMatroid = Matroid.emptyOn β

@[simp]

theorem Graph.cycleMatroid_bouquet {α : Type u_1} {β : Type u_2} (v : α) (F : Set β) : (bouquet v F).cycleMatroid = Matroid.loopyOn F

@[simp]

theorem Graph.cycleMatroid_eq_emptyOn {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.cycleMatroid = Matroid.emptyOn β ↔ G.edgeSet = ∅

theorem Graph.cycleMatroid_isFlat {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hFE : F ⊆ G.edgeSet) (hF : ∀ (H : Graph α β), H.IsCompOf (G.restrict F) → H.IsInducedSubgraph G) : G.cycleMatroid.IsFlat F

theorem Graph.orientation.isAcyclicSet_linearIndepOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {𝔽 : Type u_3} [Field 𝔽] [DecidableEq α] [DecidablePred fun (x : β) => x ∈ G.edgeSet] {I : Set β} (hI : G.IsAcyclicSet I) (D : G.orientation) : LinearIndepOn 𝔽 (D.signedIncMatrix 𝔽) I

noncomputable def Graph.cycleMatroidRep {α : Type u_1} {β : Type u_2} {G : Graph α β} (𝔽 : Type u_3) [Field 𝔽] : G.cycleMatroid.Rep 𝔽 (α → 𝔽)

Equations

• Graph.cycleMatroidRep 𝔽 = { to_fun := have hD := ⋯; hD.some.signedIncMatrix 𝔽, indep_iff' := ⋯ }

theorem Graph.cycleMatroid_representable {α : Type u_1} {β : Type u_2} {G : Graph α β} (𝔽 : Type u_3) [Field 𝔽] : G.cycleMatroid.Representable 𝔽