Walk 📖 | CompData | 45 mathmath: set_walk_length_zero_eq_of_ne, reachable_iff_nonempty_univ, Walk.map_injective_of_injective, isTree_iff_existsUnique_path, walkLengthTwoEquivCommonNeighbors_symm_apply_coe, Walk.reverse_injective, Walk.support_toPath_subset, Path.mapEmbedding_coe, Walk.reverse_surjective, card_set_walk_length_eq, Walk.default_def, Path.singleton_coe, Walk.darts_injective, reachable_iff_exists_finsetWalkLength_nonempty, Walk.darts_toPath_subset, dist_eq_sInf, set_walk_self_length_zero_eq, mem_finsetWalkLength_iff, not_reachable_iff_isEmpty_walk, adjMatrix_pow_apply_eq_card_walk, Path.isPath, Path.reverse_coe, Preconnected.set_univ_walk_nonempty, Path.notMem_edges_of_loop, coe_finsetWalkLength_eq, Walk.reverse_bijective, nonempty_of_pos_dist, set_walk_length_toFinset_eq, Walk.drop_add_heq, edist_eq_sInf, Path.nodup_support, Path.isTrail, set_walk_length_succ_eq, Walk.take_add_heq, Path.nil_coe, Path.mk'_mem_edges_singleton, IsTree.existsUnique_path, mem_finsetWalkLengthLT_iff, Walk.edges_injective, Walk.edges_toPath_subset, Path.map_coe, Walk.support_injective, coe_finsetWalkLengthLT_eq, walkLengthTwoEquivCommonNeighbors_apply_coe, Connected.set_univ_walk_nonempty
|