Commit 2023-03-01 07:31 67ba3174

View on Github →

Port/combinatorics.simple_graph.connectivity (#2514)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added def SimpleGraph.Adj.toWalk

added theorem SimpleGraph.Connected.map

added theorem SimpleGraph.Connected.set_univ_walk_nonempty

added structure SimpleGraph.Connected

added def SimpleGraph.ConnectedComponent.map

added theorem SimpleGraph.ConnectedComponent.map_comp

added theorem SimpleGraph.ConnectedComponent.map_id

added theorem SimpleGraph.ConnectedComponent.map_mk

added def SimpleGraph.ConnectedComponent

added def SimpleGraph.IsBridge

added theorem SimpleGraph.Iso.connected_iff

added theorem SimpleGraph.Iso.preconnected_iff

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 structure SimpleGraph.Walk.IsCircuit

added theorem SimpleGraph.Walk.IsCycle.not_of_nil

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 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 theorem SimpleGraph.Walk.adj_getVert_succ

added theorem SimpleGraph.Walk.adj_of_mem_edges

added def SimpleGraph.Walk.append

added theorem SimpleGraph.Walk.append_assoc

added theorem SimpleGraph.Walk.append_concat

added theorem SimpleGraph.Walk.append_copy_copy

added theorem SimpleGraph.Walk.append_nil

added def SimpleGraph.Walk.bypass

added theorem SimpleGraph.Walk.bypass_copy

added theorem SimpleGraph.Walk.bypass_isPath

added theorem SimpleGraph.Walk.chain'_adj_support

added theorem SimpleGraph.Walk.chain'_dartAdj_darts

added theorem SimpleGraph.Walk.chain_adj_support

added theorem SimpleGraph.Walk.chain_dartAdj_darts

added theorem SimpleGraph.Walk.coe_support

added theorem SimpleGraph.Walk.coe_support_append'

added theorem SimpleGraph.Walk.coe_support_append

added def SimpleGraph.Walk.concat

added def SimpleGraph.Walk.concatRec

added def SimpleGraph.Walk.concatRecAux

added theorem SimpleGraph.Walk.concatRec_concat

added theorem SimpleGraph.Walk.concatRec_nil

added theorem SimpleGraph.Walk.concat_append

added theorem SimpleGraph.Walk.concat_cons

added theorem SimpleGraph.Walk.concat_eq_append

added theorem SimpleGraph.Walk.concat_inj

added theorem SimpleGraph.Walk.concat_ne_nil

added theorem SimpleGraph.Walk.concat_nil

added theorem SimpleGraph.Walk.cons_append

added theorem SimpleGraph.Walk.cons_copy

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

added theorem SimpleGraph.Walk.cons_nil_append

added theorem SimpleGraph.Walk.cons_reverseAux

added theorem SimpleGraph.Walk.copy_cons

added theorem SimpleGraph.Walk.copy_copy

added theorem SimpleGraph.Walk.copy_nil

added theorem SimpleGraph.Walk.copy_rfl_rfl

added theorem SimpleGraph.Walk.count_edges_takeUntil_le_one

added theorem SimpleGraph.Walk.count_support_takeUntil_eq_one

added theorem SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts

added theorem SimpleGraph.Walk.dart_snd_mem_support_of_mem_darts

added def SimpleGraph.Walk.darts

added theorem SimpleGraph.Walk.darts_append

added theorem SimpleGraph.Walk.darts_bypass_subset

added theorem SimpleGraph.Walk.darts_concat

added theorem SimpleGraph.Walk.darts_cons

added theorem SimpleGraph.Walk.darts_copy

added theorem SimpleGraph.Walk.darts_dropUntil_subset

added theorem SimpleGraph.Walk.darts_map

added theorem SimpleGraph.Walk.darts_nil

added theorem SimpleGraph.Walk.darts_nodup_of_support_nodup

added theorem SimpleGraph.Walk.darts_reverse

added theorem SimpleGraph.Walk.darts_takeUntil_subset

added theorem SimpleGraph.Walk.darts_toPath_subset

added def SimpleGraph.Walk.dropUntil

added theorem SimpleGraph.Walk.dropUntil_copy

added theorem SimpleGraph.Walk.edgeSet_toSubgraph

added def SimpleGraph.Walk.edges

added theorem SimpleGraph.Walk.edges_append

added theorem SimpleGraph.Walk.edges_bypass_subset

added theorem SimpleGraph.Walk.edges_concat

added theorem SimpleGraph.Walk.edges_cons

added theorem SimpleGraph.Walk.edges_copy

added theorem SimpleGraph.Walk.edges_dropUntil_subset

added theorem SimpleGraph.Walk.edges_map

added theorem SimpleGraph.Walk.edges_nil

added theorem SimpleGraph.Walk.edges_nodup_of_support_nodup

added theorem SimpleGraph.Walk.edges_reverse

added theorem SimpleGraph.Walk.edges_subset_edgeSet

added theorem SimpleGraph.Walk.edges_takeUntil_subset

added theorem SimpleGraph.Walk.edges_toPath_subset

added theorem SimpleGraph.Walk.edges_transfer

added theorem SimpleGraph.Walk.end_mem_support

added theorem SimpleGraph.Walk.end_mem_tail_support_of_ne

added theorem SimpleGraph.Walk.eq_of_length_eq_zero

added theorem SimpleGraph.Walk.exists_boundary_dart

added theorem SimpleGraph.Walk.exists_concat_eq_cons

added theorem SimpleGraph.Walk.exists_cons_eq_concat

added theorem SimpleGraph.Walk.exists_eq_cons_of_ne

added theorem SimpleGraph.Walk.exists_length_eq_zero_iff

added theorem SimpleGraph.Walk.finite_neighborSet_toSubgraph

added theorem SimpleGraph.Walk.fst_mem_support_of_mem_edges

added def SimpleGraph.Walk.getVert

added theorem SimpleGraph.Walk.getVert_length

added theorem SimpleGraph.Walk.getVert_of_length_le

added theorem SimpleGraph.Walk.getVert_zero

added theorem SimpleGraph.Walk.isCircuit_copy

added theorem SimpleGraph.Walk.isCircuit_def

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

added def SimpleGraph.Walk.length

added theorem SimpleGraph.Walk.length_append

added theorem SimpleGraph.Walk.length_bypass_le

added theorem SimpleGraph.Walk.length_concat

added theorem SimpleGraph.Walk.length_cons

added theorem SimpleGraph.Walk.length_copy

added theorem SimpleGraph.Walk.length_darts

added theorem SimpleGraph.Walk.length_dropUntil_le

added theorem SimpleGraph.Walk.length_edges

added theorem SimpleGraph.Walk.length_eq_zero_iff

added theorem SimpleGraph.Walk.length_map

added theorem SimpleGraph.Walk.length_nil

added theorem SimpleGraph.Walk.length_reverse

added theorem SimpleGraph.Walk.length_support

added theorem SimpleGraph.Walk.length_takeUntil_le

added theorem SimpleGraph.Walk.length_transfer

added def SimpleGraph.Walk.mapLe

added theorem SimpleGraph.Walk.mapLe_isCycle

added theorem SimpleGraph.Walk.mapLe_isPath

added theorem SimpleGraph.Walk.mapLe_isTrail

added theorem SimpleGraph.Walk.map_append

added theorem SimpleGraph.Walk.map_cons

added theorem SimpleGraph.Walk.map_copy

added theorem SimpleGraph.Walk.map_eq_nil_iff

added theorem SimpleGraph.Walk.map_eq_of_eq

added theorem SimpleGraph.Walk.map_fst_darts

added theorem SimpleGraph.Walk.map_fst_darts_append

added theorem SimpleGraph.Walk.map_id

added theorem SimpleGraph.Walk.map_injective_of_injective

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

added theorem SimpleGraph.Walk.map_nil

added theorem SimpleGraph.Walk.map_snd_darts

added theorem SimpleGraph.Walk.map_toDeleteEdges_eq

added theorem SimpleGraph.Walk.mem_darts_reverse

added theorem SimpleGraph.Walk.mem_edges_toSubgraph

added theorem SimpleGraph.Walk.mem_finsetWalkLength_iff_length_eq

added theorem SimpleGraph.Walk.mem_support_append_iff

added theorem SimpleGraph.Walk.mem_support_iff

added theorem SimpleGraph.Walk.mem_support_iff_exists_append

added theorem SimpleGraph.Walk.mem_support_nil_iff

added theorem SimpleGraph.Walk.mem_tail_support_append_iff

added theorem SimpleGraph.Walk.mem_verts_toSubgraph

added theorem SimpleGraph.Walk.nil_append

added def SimpleGraph.Walk.reverse

added theorem SimpleGraph.Walk.reverse_append

added theorem SimpleGraph.Walk.reverse_concat

added theorem SimpleGraph.Walk.reverse_cons

added theorem SimpleGraph.Walk.reverse_copy

added theorem SimpleGraph.Walk.reverse_isTrail_iff

added theorem SimpleGraph.Walk.reverse_map

added theorem SimpleGraph.Walk.reverse_nil

added theorem SimpleGraph.Walk.reverse_reverse

added theorem SimpleGraph.Walk.reverse_singleton

added theorem SimpleGraph.Walk.reverse_transfer

added def SimpleGraph.Walk.rotate

added theorem SimpleGraph.Walk.rotate_darts

added theorem SimpleGraph.Walk.rotate_edges

added theorem SimpleGraph.Walk.snd_mem_support_of_mem_edges

added theorem SimpleGraph.Walk.start_mem_support

added theorem SimpleGraph.Walk.subset_support_append_left

added theorem SimpleGraph.Walk.subset_support_append_right

added def SimpleGraph.Walk.support

added theorem SimpleGraph.Walk.support_append

added theorem SimpleGraph.Walk.support_bypass_subset

added theorem SimpleGraph.Walk.support_concat

added theorem SimpleGraph.Walk.support_cons

added theorem SimpleGraph.Walk.support_copy

added theorem SimpleGraph.Walk.support_dropUntil_subset

added theorem SimpleGraph.Walk.support_eq_cons

added theorem SimpleGraph.Walk.support_map

added theorem SimpleGraph.Walk.support_ne_nil

added theorem SimpleGraph.Walk.support_nil

added theorem SimpleGraph.Walk.support_nonempty

added theorem SimpleGraph.Walk.support_reverse

added theorem SimpleGraph.Walk.support_rotate

added theorem SimpleGraph.Walk.support_takeUntil_subset

added theorem SimpleGraph.Walk.support_toPath_subset

added theorem SimpleGraph.Walk.support_transfer

added theorem SimpleGraph.Walk.tail_support_append

added def SimpleGraph.Walk.takeUntil

added theorem SimpleGraph.Walk.takeUntil_copy

added theorem SimpleGraph.Walk.take_spec

added def SimpleGraph.Walk.toDeleteEdges

added theorem SimpleGraph.Walk.toDeleteEdges_cons

added theorem SimpleGraph.Walk.toDeleteEdges_copy

added theorem SimpleGraph.Walk.toDeleteEdges_nil

added def SimpleGraph.Walk.toPath

added theorem SimpleGraph.Walk.toSubgraph_append

added theorem SimpleGraph.Walk.toSubgraph_cons_nil_eq_subgraphOfAdj

added theorem SimpleGraph.Walk.toSubgraph_map

added theorem SimpleGraph.Walk.toSubgraph_reverse

added theorem SimpleGraph.Walk.toSubgraph_rotate

added theorem SimpleGraph.Walk.transfer_append

added theorem SimpleGraph.Walk.transfer_eq_map_of_le

added theorem SimpleGraph.Walk.transfer_self

added theorem SimpleGraph.Walk.transfer_transfer

added theorem SimpleGraph.Walk.verts_toSubgraph

added inductive SimpleGraph.Walk

added theorem SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle

added theorem SimpleGraph.card_set_walk_length_eq

added theorem SimpleGraph.coe_finsetWalkLength_eq

added def SimpleGraph.connectedComponentMk

added def SimpleGraph.finsetWalkLength

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

added theorem SimpleGraph.reachable_iff_nonempty_univ

added theorem SimpleGraph.reachable_iff_reflTransGen

added theorem SimpleGraph.reachable_is_equivalence

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 theorem SimpleGraph.singletonSubgraph_connected

added theorem SimpleGraph.subgraphOfAdj_connected