Commit 2024-07-16 09:12 20524cc1

View on Github →

chore: move 300 lines off Combinatorics/SimpleGraph/Connectivity (#14647) Move material about walks as subgraphs and walk-counting to separate files. Mostly import-directed; I'm not a graph theorist - please comment if this split doesn't make sense!

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

deleted theorem SimpleGraph.Walk.edgeSet_toSubgraph

deleted theorem SimpleGraph.Walk.end_mem_verts_toSubgraph

deleted theorem SimpleGraph.Walk.finite_neighborSet_toSubgraph

deleted theorem SimpleGraph.Walk.mem_edges_toSubgraph

deleted theorem SimpleGraph.Walk.mem_finsetWalkLength_iff_length_eq

deleted theorem SimpleGraph.Walk.mem_verts_toSubgraph

deleted theorem SimpleGraph.Walk.start_mem_verts_toSubgraph

deleted theorem SimpleGraph.Walk.toSubgraph_append

deleted theorem SimpleGraph.Walk.toSubgraph_cons_nil_eq_subgraphOfAdj

deleted theorem SimpleGraph.Walk.toSubgraph_le_induce_support

deleted theorem SimpleGraph.Walk.toSubgraph_map

deleted theorem SimpleGraph.Walk.toSubgraph_reverse

deleted theorem SimpleGraph.Walk.toSubgraph_rotate

deleted theorem SimpleGraph.Walk.verts_toSubgraph

deleted theorem SimpleGraph.card_set_walk_length_eq

deleted theorem SimpleGraph.coe_finsetWalkLength_eq

deleted def SimpleGraph.finsetWalkLength

deleted theorem SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty

deleted theorem SimpleGraph.set_walk_length_succ_eq

deleted theorem SimpleGraph.set_walk_length_toFinset_eq

deleted theorem SimpleGraph.set_walk_length_zero_eq_of_ne

deleted theorem SimpleGraph.set_walk_self_length_zero_eq

deleted def SimpleGraph.walkLengthTwoEquivCommonNeighbors

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

added theorem SimpleGraph.Walk.edgeSet_toSubgraph

added theorem SimpleGraph.Walk.end_mem_verts_toSubgraph

added theorem SimpleGraph.Walk.finite_neighborSet_toSubgraph

added theorem SimpleGraph.Walk.mem_edges_toSubgraph

added theorem SimpleGraph.Walk.mem_verts_toSubgraph

added theorem SimpleGraph.Walk.start_mem_verts_toSubgraph

added theorem SimpleGraph.Walk.toSubgraph_append

added theorem SimpleGraph.Walk.toSubgraph_cons_nil_eq_subgraphOfAdj

added theorem SimpleGraph.Walk.toSubgraph_le_induce_support

added theorem SimpleGraph.Walk.toSubgraph_map

added theorem SimpleGraph.Walk.toSubgraph_reverse

added theorem SimpleGraph.Walk.toSubgraph_rotate

added theorem SimpleGraph.Walk.verts_toSubgraph

Created Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

added theorem SimpleGraph.Walk.mem_finsetWalkLength_iff_length_eq

added theorem SimpleGraph.card_set_walk_length_eq

added theorem SimpleGraph.coe_finsetWalkLength_eq

added def SimpleGraph.finsetWalkLength

added theorem SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty

added theorem SimpleGraph.set_walk_length_succ_eq

added theorem SimpleGraph.set_walk_length_toFinset_eq

added theorem SimpleGraph.set_walk_length_zero_eq_of_ne

added theorem SimpleGraph.set_walk_self_length_zero_eq

added def SimpleGraph.walkLengthTwoEquivCommonNeighbors

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean