Commit 2025-06-22 12:57 57807335

View on Github →

chore(SimpleGraph): split Combinatorics.SimpleGraph.Path (#25844) Split the long file SimpleGraph.Path.lean into two roughly equal parts.

Material on Paths, Cycles, Circuits and Trails is in Paths.lean
Material on Reachable/Preconnected/Connected/ConnectedComponents is in Connectivity.Connected

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

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

added theorem SimpleGraph.Connected.connected_delete_edge_of_not_isBridge

added theorem SimpleGraph.Connected.exists_isPath

added theorem SimpleGraph.Connected.map

added theorem SimpleGraph.Connected.set_univ_walk_nonempty

added structure SimpleGraph.Connected

added theorem SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph

added theorem SimpleGraph.ConnectedComponent.biUnion_supp_eq_supp

added theorem SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj

added theorem SimpleGraph.ConnectedComponent.connectedComponentMk_mem

added theorem SimpleGraph.ConnectedComponent.connectedComponentMk_supp_subset_supp

added theorem SimpleGraph.ConnectedComponent.connected_toSimpleGraph

added theorem SimpleGraph.ConnectedComponent.eq_of_common_vertex

added def SimpleGraph.ConnectedComponent.isoEquivSupp

added theorem SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp

added theorem SimpleGraph.ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map

added def SimpleGraph.ConnectedComponent.map

added theorem SimpleGraph.ConnectedComponent.map_comp

added theorem SimpleGraph.ConnectedComponent.map_id

added theorem SimpleGraph.ConnectedComponent.map_mk

added theorem SimpleGraph.ConnectedComponent.mem_coe_supp_of_adj

added theorem SimpleGraph.ConnectedComponent.mem_supp_congr_adj

added theorem SimpleGraph.ConnectedComponent.mem_supp_iff

added theorem SimpleGraph.ConnectedComponent.mem_supp_of_adj_mem_supp

added theorem SimpleGraph.ConnectedComponent.nonempty_supp

added theorem SimpleGraph.ConnectedComponent.reachable_of_mem_supp

added theorem SimpleGraph.ConnectedComponent.reachable_toSimpleGraph

added def SimpleGraph.ConnectedComponent.recOn

added def SimpleGraph.ConnectedComponent.supp

added theorem SimpleGraph.ConnectedComponent.supp_inj

added theorem SimpleGraph.ConnectedComponent.supp_injective

added def SimpleGraph.ConnectedComponent.toSimpleGraph

added theorem SimpleGraph.ConnectedComponent.toSimpleGraph_adj

added def SimpleGraph.ConnectedComponent.toSimpleGraph_hom

added theorem SimpleGraph.ConnectedComponent.toSimpleGraph_hom_apply

added theorem SimpleGraph.ConnectedComponent.top_supp_eq_univ

added def SimpleGraph.ConnectedComponent

added def SimpleGraph.IsBridge

added def SimpleGraph.Iso.connectedComponentEquiv

added theorem SimpleGraph.Iso.connectedComponentEquiv_refl

added theorem SimpleGraph.Iso.connectedComponentEquiv_symm

added theorem SimpleGraph.Iso.connectedComponentEquiv_trans

added theorem SimpleGraph.Iso.connected_iff

added theorem SimpleGraph.Iso.preconnected_iff

added theorem SimpleGraph.Iso.reachable_iff

added theorem SimpleGraph.Iso.symm_apply_reachable

added theorem SimpleGraph.Preconnected.exists_isPath

added theorem SimpleGraph.Preconnected.map

added theorem SimpleGraph.Preconnected.set_univ_walk_nonempty

added theorem SimpleGraph.Preconnected.subsingleton_connectedComponent

added theorem SimpleGraph.Preconnected.support_eq_univ

added def SimpleGraph.Preconnected

added theorem SimpleGraph.Reachable.exists_isPath

added theorem SimpleGraph.Reachable.mem_subgraphVerts

added def SimpleGraph.Reachable

added theorem SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle

added theorem SimpleGraph.adj_of_mem_walk_support

added theorem SimpleGraph.bot_not_connected

added theorem SimpleGraph.bot_not_preconnected

added theorem SimpleGraph.bot_preconnected

added theorem SimpleGraph.bot_preconnected_iff_subsingleton

added def SimpleGraph.connectedComponentMk

added theorem SimpleGraph.connected_iff_exists_forall_reachable

added theorem SimpleGraph.iUnion_connectedComponentSupp

added theorem SimpleGraph.isBridge_iff

added theorem SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem

added theorem SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges

added theorem SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem

added theorem SimpleGraph.mem_support_of_mem_walk_support

added theorem SimpleGraph.mem_support_of_reachable

added theorem SimpleGraph.not_reachable_iff_isEmpty_walk

added theorem SimpleGraph.pairwise_disjoint_supp_connectedComponent

added def SimpleGraph.reachableSetoid

added theorem SimpleGraph.reachable_bot

added theorem SimpleGraph.reachable_comm

added theorem SimpleGraph.reachable_deleteEdges_iff_exists_cycle.aux

added theorem SimpleGraph.reachable_delete_edges_iff_exists_walk

added theorem SimpleGraph.reachable_iff_nonempty_univ

added theorem SimpleGraph.reachable_iff_reflTransGen

added theorem SimpleGraph.reachable_is_equivalence

added theorem SimpleGraph.top_connected

added theorem SimpleGraph.top_preconnected

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

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

Modified Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

deleted theorem SimpleGraph.Connected.connected_delete_edge_of_not_isBridge

deleted theorem SimpleGraph.Connected.exists_isPath

deleted theorem SimpleGraph.Connected.map

deleted theorem SimpleGraph.Connected.set_univ_walk_nonempty

deleted structure SimpleGraph.Connected

deleted theorem SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph

deleted theorem SimpleGraph.ConnectedComponent.biUnion_supp_eq_supp

deleted theorem SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj

deleted theorem SimpleGraph.ConnectedComponent.connectedComponentMk_mem

deleted theorem SimpleGraph.ConnectedComponent.connectedComponentMk_supp_subset_supp

deleted theorem SimpleGraph.ConnectedComponent.connected_toSimpleGraph

deleted theorem SimpleGraph.ConnectedComponent.eq_of_common_vertex

deleted def SimpleGraph.ConnectedComponent.isoEquivSupp

deleted theorem SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp

deleted theorem SimpleGraph.ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map

deleted def SimpleGraph.ConnectedComponent.map

deleted theorem SimpleGraph.ConnectedComponent.map_comp

deleted theorem SimpleGraph.ConnectedComponent.map_id

deleted theorem SimpleGraph.ConnectedComponent.map_mk

deleted theorem SimpleGraph.ConnectedComponent.mem_coe_supp_of_adj

deleted theorem SimpleGraph.ConnectedComponent.mem_supp_congr_adj

deleted theorem SimpleGraph.ConnectedComponent.mem_supp_iff

deleted theorem SimpleGraph.ConnectedComponent.mem_supp_of_adj_mem_supp

deleted theorem SimpleGraph.ConnectedComponent.nonempty_supp

deleted theorem SimpleGraph.ConnectedComponent.reachable_of_mem_supp

deleted theorem SimpleGraph.ConnectedComponent.reachable_toSimpleGraph

deleted def SimpleGraph.ConnectedComponent.recOn

deleted def SimpleGraph.ConnectedComponent.supp

deleted theorem SimpleGraph.ConnectedComponent.supp_inj

deleted theorem SimpleGraph.ConnectedComponent.supp_injective

deleted def SimpleGraph.ConnectedComponent.toSimpleGraph

deleted theorem SimpleGraph.ConnectedComponent.toSimpleGraph_adj

deleted def SimpleGraph.ConnectedComponent.toSimpleGraph_hom

deleted theorem SimpleGraph.ConnectedComponent.toSimpleGraph_hom_apply

deleted theorem SimpleGraph.ConnectedComponent.top_supp_eq_univ

deleted def SimpleGraph.ConnectedComponent

deleted def SimpleGraph.IsBridge

deleted def SimpleGraph.Iso.connectedComponentEquiv

deleted theorem SimpleGraph.Iso.connectedComponentEquiv_refl

deleted theorem SimpleGraph.Iso.connectedComponentEquiv_symm

deleted theorem SimpleGraph.Iso.connectedComponentEquiv_trans

deleted theorem SimpleGraph.Iso.connected_iff

deleted theorem SimpleGraph.Iso.preconnected_iff

deleted theorem SimpleGraph.Iso.reachable_iff

deleted theorem SimpleGraph.Iso.symm_apply_reachable

deleted theorem SimpleGraph.Path.cons_isCycle

deleted theorem SimpleGraph.Path.count_edges_eq_one

deleted theorem SimpleGraph.Path.count_support_eq_one

deleted theorem SimpleGraph.Path.loop_eq

deleted theorem SimpleGraph.Path.mapEmbedding_injective

deleted theorem SimpleGraph.Path.map_injective

deleted theorem SimpleGraph.Path.mk'_mem_edges_singleton

deleted theorem SimpleGraph.Path.nodup_support

deleted theorem SimpleGraph.Path.notMem_edges_of_loop

deleted def SimpleGraph.Path.reverse

deleted def SimpleGraph.Path.singleton

deleted theorem SimpleGraph.Preconnected.exists_isPath

deleted theorem SimpleGraph.Preconnected.map

deleted theorem SimpleGraph.Preconnected.set_univ_walk_nonempty

deleted theorem SimpleGraph.Preconnected.subsingleton_connectedComponent

deleted theorem SimpleGraph.Preconnected.support_eq_univ

deleted def SimpleGraph.Preconnected

deleted theorem SimpleGraph.Reachable.exists_isPath

deleted theorem SimpleGraph.Reachable.mem_subgraphVerts

deleted def SimpleGraph.Reachable

deleted theorem SimpleGraph.Walk.IsCircuit.not_nil

deleted structure SimpleGraph.Walk.IsCircuit

deleted theorem SimpleGraph.Walk.IsCycle.getVert_endpoint_iff

deleted theorem SimpleGraph.Walk.IsCycle.getVert_injOn'

deleted theorem SimpleGraph.Walk.IsCycle.getVert_injOn

deleted theorem SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one

deleted theorem SimpleGraph.Walk.IsCycle.isPath_of_append_left

deleted theorem SimpleGraph.Walk.IsCycle.isPath_of_append_right

deleted theorem SimpleGraph.Walk.IsCycle.isPath_takeUntil

deleted theorem SimpleGraph.Walk.IsCycle.ne_bot

deleted theorem SimpleGraph.Walk.IsCycle.not_nil

deleted theorem SimpleGraph.Walk.IsCycle.not_of_nil

deleted theorem SimpleGraph.Walk.IsCycle.snd_ne_penultimate

deleted theorem SimpleGraph.Walk.IsCycle.three_le_length

deleted structure SimpleGraph.Walk.IsCycle

deleted theorem SimpleGraph.Walk.IsPath.getVert_eq_end_iff

deleted theorem SimpleGraph.Walk.IsPath.getVert_eq_start_iff

deleted theorem SimpleGraph.Walk.IsPath.getVert_injOn

deleted theorem SimpleGraph.Walk.IsPath.getVert_injOn_iff

deleted theorem SimpleGraph.Walk.IsPath.length_lt

deleted theorem SimpleGraph.Walk.IsPath.mk'

deleted theorem SimpleGraph.Walk.IsPath.nil

deleted theorem SimpleGraph.Walk.IsPath.of_adj

deleted theorem SimpleGraph.Walk.IsPath.of_append_left

deleted theorem SimpleGraph.Walk.IsPath.of_append_right

deleted theorem SimpleGraph.Walk.IsPath.of_cons

deleted theorem SimpleGraph.Walk.IsPath.reverse

deleted theorem SimpleGraph.Walk.IsPath.tail

deleted structure SimpleGraph.Walk.IsPath

deleted theorem SimpleGraph.Walk.IsTrail.count_edges_eq_one

deleted theorem SimpleGraph.Walk.IsTrail.count_edges_le_one

deleted theorem SimpleGraph.Walk.IsTrail.length_le_card_edgeFinset

deleted theorem SimpleGraph.Walk.IsTrail.nil

deleted theorem SimpleGraph.Walk.IsTrail.of_append_left

deleted theorem SimpleGraph.Walk.IsTrail.of_append_right

deleted theorem SimpleGraph.Walk.IsTrail.of_cons

deleted theorem SimpleGraph.Walk.IsTrail.reverse

deleted structure SimpleGraph.Walk.IsTrail

deleted def SimpleGraph.Walk.bypass

deleted theorem SimpleGraph.Walk.bypass_copy

deleted theorem SimpleGraph.Walk.bypass_eq_self_of_length_le

deleted theorem SimpleGraph.Walk.bypass_isPath

deleted theorem SimpleGraph.Walk.cons_isCycle_iff

deleted theorem SimpleGraph.Walk.cons_isPath_iff

deleted theorem SimpleGraph.Walk.cons_isTrail_iff

deleted theorem SimpleGraph.Walk.darts_bypass_subset

deleted theorem SimpleGraph.Walk.darts_toPath_subset

deleted theorem SimpleGraph.Walk.edges_bypass_subset

deleted theorem SimpleGraph.Walk.edges_toPath_subset

deleted theorem SimpleGraph.Walk.endpoint_notMem_support_takeUntil

deleted theorem SimpleGraph.Walk.isCircuit_copy

deleted theorem SimpleGraph.Walk.isCycle_copy

deleted theorem SimpleGraph.Walk.isCycle_def

deleted theorem SimpleGraph.Walk.isCycle_reverse

deleted theorem SimpleGraph.Walk.isPath_copy

deleted theorem SimpleGraph.Walk.isPath_def

deleted theorem SimpleGraph.Walk.isPath_iff_eq_nil

deleted theorem SimpleGraph.Walk.isPath_reverse_iff

deleted theorem SimpleGraph.Walk.isTrail_copy

deleted theorem SimpleGraph.Walk.length_bypass_le

deleted theorem SimpleGraph.Walk.mapLe_isCycle

deleted theorem SimpleGraph.Walk.mapLe_isPath

deleted theorem SimpleGraph.Walk.mapLe_isTrail

deleted theorem SimpleGraph.Walk.map_isCycle_iff_of_injective

deleted theorem SimpleGraph.Walk.map_isPath_iff_of_injective

deleted theorem SimpleGraph.Walk.map_isPath_of_injective

deleted theorem SimpleGraph.Walk.map_isTrail_iff_of_injective

deleted theorem SimpleGraph.Walk.not_nil_of_isCycle_cons

deleted theorem SimpleGraph.Walk.reverse_isTrail_iff

deleted theorem SimpleGraph.Walk.support_bypass_subset

deleted theorem SimpleGraph.Walk.support_toPath_subset

deleted theorem SimpleGraph.Walk.toDeleteEdges_copy

deleted def SimpleGraph.Walk.toPath

deleted theorem SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle

deleted theorem SimpleGraph.adj_of_mem_walk_support

deleted theorem SimpleGraph.bot_not_connected

deleted theorem SimpleGraph.bot_not_preconnected

deleted theorem SimpleGraph.bot_preconnected

deleted theorem SimpleGraph.bot_preconnected_iff_subsingleton

deleted def SimpleGraph.connectedComponentMk

deleted theorem SimpleGraph.connected_iff_exists_forall_reachable

deleted theorem SimpleGraph.iUnion_connectedComponentSupp

deleted theorem SimpleGraph.isBridge_iff

deleted theorem SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem

deleted theorem SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges

deleted theorem SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem

deleted theorem SimpleGraph.mem_support_of_mem_walk_support

deleted theorem SimpleGraph.mem_support_of_reachable

deleted theorem SimpleGraph.not_reachable_iff_isEmpty_walk

deleted theorem SimpleGraph.pairwise_disjoint_supp_connectedComponent

deleted def SimpleGraph.reachableSetoid

deleted theorem SimpleGraph.reachable_bot

deleted theorem SimpleGraph.reachable_comm

deleted theorem SimpleGraph.reachable_deleteEdges_iff_exists_cycle.aux

deleted theorem SimpleGraph.reachable_delete_edges_iff_exists_walk

deleted theorem SimpleGraph.reachable_iff_nonempty_univ

deleted theorem SimpleGraph.reachable_iff_reflTransGen

deleted theorem SimpleGraph.reachable_is_equivalence

deleted theorem SimpleGraph.top_connected

deleted theorem SimpleGraph.top_preconnected

Created Mathlib/Combinatorics/SimpleGraph/Paths.lean

added theorem SimpleGraph.Path.cons_isCycle

added theorem SimpleGraph.Path.count_edges_eq_one

added theorem SimpleGraph.Path.count_support_eq_one

added theorem SimpleGraph.Path.loop_eq

added theorem SimpleGraph.Path.mapEmbedding_injective

added theorem SimpleGraph.Path.map_injective

added theorem SimpleGraph.Path.mk'_mem_edges_singleton

added theorem SimpleGraph.Path.nodup_support

added theorem SimpleGraph.Path.notMem_edges_of_loop

added def SimpleGraph.Path.reverse

added def SimpleGraph.Path.singleton

added theorem SimpleGraph.Walk.IsCircuit.not_nil

added structure SimpleGraph.Walk.IsCircuit

added theorem SimpleGraph.Walk.IsCycle.getVert_endpoint_iff

added theorem SimpleGraph.Walk.IsCycle.getVert_injOn'

added theorem SimpleGraph.Walk.IsCycle.getVert_injOn

added theorem SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one

added theorem SimpleGraph.Walk.IsCycle.isPath_of_append_left

added theorem SimpleGraph.Walk.IsCycle.isPath_of_append_right

added theorem SimpleGraph.Walk.IsCycle.isPath_takeUntil

added theorem SimpleGraph.Walk.IsCycle.ne_bot

added theorem SimpleGraph.Walk.IsCycle.not_nil

added theorem SimpleGraph.Walk.IsCycle.not_of_nil

added theorem SimpleGraph.Walk.IsCycle.snd_ne_penultimate

added theorem SimpleGraph.Walk.IsCycle.three_le_length

added structure SimpleGraph.Walk.IsCycle

added theorem SimpleGraph.Walk.IsPath.getVert_eq_end_iff

added theorem SimpleGraph.Walk.IsPath.getVert_eq_start_iff

added theorem SimpleGraph.Walk.IsPath.getVert_injOn

added theorem SimpleGraph.Walk.IsPath.getVert_injOn_iff

added theorem SimpleGraph.Walk.IsPath.length_lt

added theorem SimpleGraph.Walk.IsPath.mk'

added theorem SimpleGraph.Walk.IsPath.nil

added theorem SimpleGraph.Walk.IsPath.of_adj

added theorem SimpleGraph.Walk.IsPath.of_append_left

added theorem SimpleGraph.Walk.IsPath.of_append_right

added theorem SimpleGraph.Walk.IsPath.of_cons

added theorem SimpleGraph.Walk.IsPath.reverse

added theorem SimpleGraph.Walk.IsPath.tail

added structure SimpleGraph.Walk.IsPath

added theorem SimpleGraph.Walk.IsTrail.count_edges_eq_one

added theorem SimpleGraph.Walk.IsTrail.count_edges_le_one

added theorem SimpleGraph.Walk.IsTrail.length_le_card_edgeFinset

added theorem SimpleGraph.Walk.IsTrail.nil

added theorem SimpleGraph.Walk.IsTrail.of_append_left

added theorem SimpleGraph.Walk.IsTrail.of_append_right

added theorem SimpleGraph.Walk.IsTrail.of_cons

added theorem SimpleGraph.Walk.IsTrail.reverse

added structure SimpleGraph.Walk.IsTrail

added def SimpleGraph.Walk.bypass

added theorem SimpleGraph.Walk.bypass_copy

added theorem SimpleGraph.Walk.bypass_eq_self_of_length_le

added theorem SimpleGraph.Walk.bypass_isPath

added theorem SimpleGraph.Walk.cons_isCycle_iff

added theorem SimpleGraph.Walk.cons_isPath_iff

added theorem SimpleGraph.Walk.cons_isTrail_iff

added theorem SimpleGraph.Walk.darts_bypass_subset

added theorem SimpleGraph.Walk.darts_toPath_subset

added theorem SimpleGraph.Walk.edges_bypass_subset

added theorem SimpleGraph.Walk.edges_toPath_subset

added theorem SimpleGraph.Walk.endpoint_notMem_support_takeUntil

added theorem SimpleGraph.Walk.isCircuit_copy

added theorem SimpleGraph.Walk.isCycle_copy

added theorem SimpleGraph.Walk.isCycle_def

added theorem SimpleGraph.Walk.isCycle_reverse

added theorem SimpleGraph.Walk.isPath_copy

added theorem SimpleGraph.Walk.isPath_def

added theorem SimpleGraph.Walk.isPath_iff_eq_nil

added theorem SimpleGraph.Walk.isPath_reverse_iff

added theorem SimpleGraph.Walk.isTrail_copy

added theorem SimpleGraph.Walk.length_bypass_le

added theorem SimpleGraph.Walk.mapLe_isCycle

added theorem SimpleGraph.Walk.mapLe_isPath

added theorem SimpleGraph.Walk.mapLe_isTrail

added theorem SimpleGraph.Walk.map_isCycle_iff_of_injective

added theorem SimpleGraph.Walk.map_isPath_iff_of_injective

added theorem SimpleGraph.Walk.map_isPath_of_injective

added theorem SimpleGraph.Walk.map_isTrail_iff_of_injective

added theorem SimpleGraph.Walk.not_nil_of_isCycle_cons

added theorem SimpleGraph.Walk.reverse_isTrail_iff

added theorem SimpleGraph.Walk.support_bypass_subset

added theorem SimpleGraph.Walk.support_toPath_subset

added theorem SimpleGraph.Walk.toDeleteEdges_copy

added def SimpleGraph.Walk.toPath

Modified Mathlib/Combinatorics/SimpleGraph/Prod.lean

Modified Mathlib/Combinatorics/SimpleGraph/Trails.lean