Commit 2023-08-14 12:56 86bb3de9

View on Github →

feat: lemmas about connectivity of subgraphs and induced graphs (#5927) (Replaces [mathlib#18454](https://github.com/leanprover-community/mathlib/pull/18454).)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

deleted def SimpleGraph.InduceHom

modified theorem SimpleGraph.coe_induceHom

added def SimpleGraph.induceHom

added def SimpleGraph.induceHomOfLE

added theorem SimpleGraph.induceHomOfLE_apply

added theorem SimpleGraph.induceHomOfLE_toHom

added theorem SimpleGraph.induceHom_injective

added theorem SimpleGraph.induce_singleton_eq_top

added theorem SimpleGraph.le_comap_of_subsingleton

added theorem SimpleGraph.map_le_of_subsingleton

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added theorem SimpleGraph.Walk.end_mem_verts_toSubgraph

added theorem SimpleGraph.Walk.start_mem_verts_toSubgraph

added theorem SimpleGraph.Walk.toSubgraph_le_induce_support

added theorem SimpleGraph.connected_iff_exists_forall_reachable

deleted theorem SimpleGraph.singletonSubgraph_connected

deleted theorem SimpleGraph.subgraphOfAdj_connected

added theorem SimpleGraph.top_connected

added theorem SimpleGraph.top_preconnected

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

added theorem SimpleGraph.Subgraph.Connected.adj_union

added theorem SimpleGraph.Subgraph.Connected.induce_verts

added theorem SimpleGraph.Subgraph.connected_iff_forall_exists_walk_subgraph

added theorem SimpleGraph.Subgraph.induce_union_connected

added theorem SimpleGraph.Subgraph.preconnected_iff_forall_exists_walk_subgraph

added theorem SimpleGraph.Subgraph.singletonSubgraph_connected

added theorem SimpleGraph.Subgraph.subgraphOfAdj_connected

added theorem SimpleGraph.Subgraph.top_induce_pair_connected_of_adj

added theorem SimpleGraph.Walk.connected_induce_support

added theorem SimpleGraph.Walk.toSubgraph_connected

added theorem SimpleGraph.connected_induce_iff

added theorem SimpleGraph.extend_finset_to_connected

added theorem SimpleGraph.induce_connected_adj_union

added theorem SimpleGraph.induce_connected_of_patches

added theorem SimpleGraph.induce_pair_connected_of_adj

added theorem SimpleGraph.induce_sUnion_connected_of_pairwise_not_disjoint

added theorem SimpleGraph.induce_union_connected

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

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added theorem SimpleGraph.Subgraph.coeSubgraph_Adj

added theorem SimpleGraph.Subgraph.coeSubgraph_le

added theorem SimpleGraph.Subgraph.coeSubgraph_restrict_eq

added theorem SimpleGraph.Subgraph.coe_hom

added theorem SimpleGraph.Subgraph.le_induce_top_verts

added theorem SimpleGraph.Subgraph.le_induce_union

added theorem SimpleGraph.Subgraph.le_induce_union_left

added theorem SimpleGraph.Subgraph.le_induce_union_right

added theorem SimpleGraph.Subgraph.restrict_Adj

added theorem SimpleGraph.subgraphOfAdj_le_of_adj