Theorems · Definition · combinatorics
SimpleGraph.IsCycles
{V : Type u_1} → SimpleGraph V → PropA graph G consists of a set of cycles, if each vertex is either isolated or connected to
exactly two vertices. This is used to create new matchings by taking the symmDiff with cycles.
The definition of symmDiff that makes sense is the one for SimpleGraph. The symmDiff
for SimpleGraph.Subgraph deriving from the lattice structure also affects the vertices included,
which we do not want in this case. This is why this property is defined for SimpleGraph, rather
than SimpleGraph.Subgraph.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement and proof · cited by 3,072
- Set.Nonemptyproof · cited by 2,627
- Set.ncardproof · cited by 344
- SimpleGraph.neighborSetproof · cited by 257
Cited by12
Results whose statement or proof uses this declaration.
- SimpleGraph.IsCycles.other_adj_of_adjstatement and proof · cited by 2
- SimpleGraph.IsCycles.reachable_deleteEdgesstatement and proof · cited by 1
- SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoestatement and proof · cited by 1
- SimpleGraph.Walk.IsCycle.isCycles_spanningCoe_toSubgraphstatement · cited by 1
- SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edgestatement · cited by 0
- SimpleGraph.Walk.IsCycle.adj_toSubgraph_iff_of_isCyclesstatement and proof · cited by 0
- SimpleGraph.IsCycles.existsUnique_ne_adjstatement and proof · cited by 0
- SimpleGraph.IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSuppstatement and proof · cited by 0
- SimpleGraph.IsCycles.snd_of_mem_support_of_isPath_of_adjstatement and proof · cited by 0
- SimpleGraph.IsCycles.toSimpleGraphstatement and proof · cited by 0
- SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_isCyclesstatement · cited by 0
- SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_of_isAlternatingstatement and proof · cited by 0