Commit 2024-07-30 05:14 2609c03c

View on Github →

refactor(Combinatorics/SimpleGraph): move Walk to its own file (#15171) split Path and higher into a separate file from Walk

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

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

Created Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.Connected.map

added theorem SimpleGraph.Connected.set_univ_walk_nonempty

added structure SimpleGraph.Connected

added theorem SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj

added theorem SimpleGraph.ConnectedComponent.connectedComponentMk_mem

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_iff

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

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.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.not_mem_edges_of_loop

added def SimpleGraph.Path.reverse

added def SimpleGraph.Path.singleton

added theorem SimpleGraph.Preconnected.map

added theorem SimpleGraph.Preconnected.set_univ_walk_nonempty

added theorem SimpleGraph.Preconnected.subsingleton_connectedComponent

added def SimpleGraph.Preconnected

added def SimpleGraph.Reachable

added theorem SimpleGraph.Walk.IsCircuit.not_nil

added structure SimpleGraph.Walk.IsCircuit

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.three_le_length

added structure SimpleGraph.Walk.IsCycle

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_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.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.isCircuit_copy

added theorem SimpleGraph.Walk.isCycle_copy

added theorem SimpleGraph.Walk.isCycle_def

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.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

added theorem SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle

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_not_mem

added theorem SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges

added theorem SimpleGraph.isBridge_iff_mem_and_forall_cycle_not_mem

added theorem SimpleGraph.not_reachable_iff_isEmpty_walk

added theorem SimpleGraph.pairwise_disjoint_supp_connectedComponent

added def SimpleGraph.reachableSetoid

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/Prod.lean

Modified Mathlib/Combinatorics/SimpleGraph/Trails.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

deleted theorem SimpleGraph.Connected.map

deleted theorem SimpleGraph.Connected.set_univ_walk_nonempty

deleted structure SimpleGraph.Connected

deleted theorem SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj

deleted theorem SimpleGraph.ConnectedComponent.connectedComponentMk_mem

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_iff

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

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.not_mem_edges_of_loop

deleted def SimpleGraph.Path.reverse

deleted def SimpleGraph.Path.singleton

deleted theorem SimpleGraph.Preconnected.map

deleted theorem SimpleGraph.Preconnected.set_univ_walk_nonempty

deleted theorem SimpleGraph.Preconnected.subsingleton_connectedComponent

deleted def SimpleGraph.Preconnected

deleted def SimpleGraph.Reachable

deleted theorem SimpleGraph.Walk.IsCircuit.not_nil

deleted structure SimpleGraph.Walk.IsCircuit

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.three_le_length

deleted structure SimpleGraph.Walk.IsCycle

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_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.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.isCircuit_copy

deleted theorem SimpleGraph.Walk.isCycle_copy

deleted theorem SimpleGraph.Walk.isCycle_def

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.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 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_not_mem

deleted theorem SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges

deleted theorem SimpleGraph.isBridge_iff_mem_and_forall_cycle_not_mem

deleted theorem SimpleGraph.not_reachable_iff_isEmpty_walk

deleted theorem SimpleGraph.pairwise_disjoint_supp_connectedComponent

deleted def SimpleGraph.reachableSetoid

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

Modified scripts/style-exceptions.txt