Walk 📖 | CompData | 81 mathmath: Reachable.exists_isPath, exists_girth_eq_length, set_walk_length_zero_eq_of_ne, reachable_iff_nonempty_univ, Walk.map_injective_of_injective, isTree_iff_existsUnique_path, Walk.exists_eq_cons_of_ne, walkLengthTwoEquivCommonNeighbors_symm_apply_coe, Walk.reverse_injective, Walk.support_toPath_subset, Path.mapEmbedding_coe, Walk.reverse_surjective, Walk.exists_isTrail_forall_isTrail_length_le_length, card_set_walk_length_eq, exists_egirth_eq_length, Walk.exists_concat_eq_cons, Walk.default_def, is3Clique_iff_exists_cycle_length_three, Path.singleton_coe, Walk.darts_injective, reachable_iff_exists_finsetWalkLength_nonempty, reachable_delete_edges_iff_exists_walk, Walk.darts_toPath_subset, adj_and_reachable_delete_edges_iff_exists_cycle, Connected.exists_walk_length_eq_dist, dist_eq_sInf, Path.count_edges_eq_one, set_walk_self_length_zero_eq, mem_finsetWalkLength_iff, Connected.exists_isPath, Walk.not_nil_iff, not_reachable_iff_isEmpty_walk, adjMatrix_pow_apply_eq_card_walk, Path.count_support_eq_one, Path.isPath, Path.reverse_coe, Preconnected.set_univ_walk_nonempty, Subgraph.connected_iff_forall_exists_walk_subgraph, Path.notMem_edges_of_loop, coe_finsetWalkLength_eq, Walk.reverse_bijective, Walk.mem_support_iff_exists_append, nonempty_of_pos_dist, Connected.exists_path_of_dist, set_walk_length_toFinset_eq, Walk.drop_add_heq, edist_eq_sInf, exists_isCycle_of_two_le_isEdgeReachable, Connected.exists_walk_length_eq_edist, Path.nodup_support, Path.isTrail, Walk.exists_isPath_forall_isPath_length_le_length, set_walk_length_succ_eq, Walk.take_add_heq, Walk.exists_length_eq_zero_iff, Walk.IsPath.mem_support_iff_exists_append, Path.nil_coe, Walk.exists_cons_eq_concat, Subgraph.preconnected_iff_forall_exists_walk_subgraph, Path.mk'_mem_edges_singleton, IsTree.existsUnique_path, Walk.IsCycle.exists_isCycle_snd_verts_eq, Reachable.exists_walk_length_eq_dist, exists_walk_of_edist_ne_top, mem_finsetWalkLengthLT_iff, Walk.edges_injective, Walk.edges_toPath_subset, Path.map_coe, exists_walk_of_edist_eq_coe, Preconnected.exists_isPath, Path.cons_isCycle, Walk.support_injective, Reachable.exists_walk_length_eq_edist, coe_finsetWalkLengthLT_eq, exists_walk_of_dist_ne_zero, walkLengthTwoEquivCommonNeighbors_apply_coe, Walk.nil_isSubwalk_iff_exists, IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp, Walk.exists_length_eq_one_iff, Reachable.exists_path_of_dist, Connected.set_univ_walk_nonempty
|