Theoremsreachable, connected_delete_edge_of_not_isBridge, exists_isPath, map, mono, nonempty, of_subsingleton, preconnected, set_univ_walk_nonempty, adj_spanningCoe_toSimpleGraph, biUnion_supp_eq_supp, connectedComponentMk_eq_of_adj, connectedComponentMk_mem, connectedComponentMk_supp_subset_supp, connected_toSimpleGraph, eq, eq_of_common_vertex, exact, exists, forall, ind, ind₂, inhabited_default, instFinite, instNonempty, instSubsingleton, isEmpty, iso_image_comp_eq_map_iff_eq_comp, iso_inv_image_comp_eq_iff_eq_map, lift_mk, map_comp, map_id, map_mk, maximal_connected_induce_iff, maximal_connected_induce_supp, mem_coe_supp_of_adj, mem_supp_congr_adj, mem_supp_iff, mem_supp_of_adj_mem_supp, nonempty_supp, reachable_of_mem_supp, reachable_toSimpleGraph, sound, supp_inj, supp_injective, supp_injective_iff, surjective_map_ofLE, toSimpleGraph_adj, toSimpleGraph_hom_apply, top_supp_eq_univ, anti_of_mem_edgeSet, sup_fromEdgeSet_of_not_reachable, sup_fromEdgeSet_of_not_reachable_of_isBridge, connectedComponentEquiv_apply, connectedComponentEquiv_refl, connectedComponentEquiv_symm, connectedComponentEquiv_symm_apply, connectedComponentEquiv_trans, connected_iff, preconnected_iff, reachable_iff, symm_apply_reachable, degree_pos_of_nontrivial, exists_adj_of_nontrivial, exists_isPath, induce_of_degree_eq_one, map, minDegree_pos_of_nontrivial, mono, of_subsingleton, set_univ_walk_nonempty, subsingleton_connectedComponent, support_eq_univ, degree_pos_left, degree_pos_right, elim, elim_path, exists_isPath, map, mem_subgraphVerts, mono, mono', nonempty_neighborSet_left, nonempty_neighborSet_right, of_subsingleton, refl, rfl, trans, not_mem_edges_of_not_reachable, not_mem_support_of_not_reachable, not_mem_support_of_subsingleton_neighborSet, exists_mem_edges_of_not_reachable_deleteEdges, mem_edges_of_not_reachable_deleteEdges, reachable, adj_and_reachable_delete_edges_iff_exists_cycle, adj_le_reachable, adj_of_mem_walk_support, connected_bot_iff, connected_iff, connected_iff_exists_forall_reachable, connected_or_connected_compl, connected_or_preconnected_compl, connected_top, connected_top_iff, homOfConnectedComponents_apply, iUnion_connectedComponentSupp, isBridge_iff, isBridge_iff_adj_and_forall_cycle_notMem, isBridge_iff_adj_and_forall_walk_mem_edges, isBridge_iff_mem_and_forall_cycle_notMem, mem_support_of_mem_walk_support, mem_support_of_reachable, not_connected_bot, not_preconnected_bot, not_reachable_iff_isEmpty_walk, not_reachable_of_left_degree_zero, not_reachable_of_neighborSet_left_eq_empty, not_reachable_of_neighborSet_right_eq_empty, not_reachable_of_right_degree_zero, pairwise_disjoint_supp_connectedComponent, preconnected_bot, preconnected_bot_iff_subsingleton, preconnected_iff_reachable_eq_top, preconnected_top, reachable_bot, reachable_comm, aux, reachable_delete_edges_iff_exists_walk, reachable_eq_reflTransGen, reachable_fromEdgeSet_eq_reflTransGen_toRel, reachable_fromEdgeSet_fromRel_eq_reflTransGen, reachable_iff_nonempty_univ, reachable_iff_reflTransGen, reachable_is_equivalence, reachable_or_compl_adj, reachable_or_reachable_compl, reachable_top | 137 |