Commit 2025-02-14 14:20 d202dedb

View on Github →

feat(Combinatorics/SimpleGraph): Characterizing SimpleGraph.IsCycles (#20830) Shows that IsCycles is appropriately named. The core result is IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponent_supp, which shows that for an edge in a nontrivial component a cycle can be constructed that has exactly the edges of the component. In order to get this some API is included:

Coercions of walks in graphs that are the result of coerced subgraphs
NeighborSets of toSubgraph for paths
Supporting results for IsCycles
Some miscellaneous supporting lemma's This is all in preparation for Tutte's theorem.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

added theorem SimpleGraph.Subgraph.Connected.exists_verts_eq_connectedComponentSupp

added theorem SimpleGraph.Walk.IsPath.ncard_neighborSet_toSubgraph_internal_eq_two

added theorem SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_endpoint

added theorem SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_internal

added theorem SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_startpoint

added theorem SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

added theorem SimpleGraph.IsCycles.existsUnique_ne_adj

added theorem SimpleGraph.IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp

added theorem SimpleGraph.IsCycles.reachable_deleteEdges

added theorem SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoe

added theorem SimpleGraph.IsCycles.snd_of_mem_support_of_isPath_of_adj

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.Reachable.mem_subgraphVerts

added theorem SimpleGraph.Walk.IsPath.of_adj

modified theorem SimpleGraph.reachable_delete_edges_iff_exists_walk

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added theorem SimpleGraph.Subgraph.adj_iff_of_neighborSet_equiv

added theorem SimpleGraph.Subgraph.spanningCoe_subgraphOfAdj

added theorem SimpleGraph.Subgraph.sup_spanningCoe

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.penultimate_reverse

added theorem SimpleGraph.Walk.snd_reverse