| Name | Category | Theorems |
|---|
Nil 📖 | CompData | 24 mathmath: nil_take_iff, nil_copy, nil_iff_support_eq, nil_iff_eq_nil, nil_iff_length_eq, IsCircuit.not_nil, nil_append_iff, nil_drop_of_length_le, nil_of_subsingleton, not_nil_iff, not_nil_cons, nil_drop_iff, getLast_darts_eq_lastDart, not_nil_of_adj_toSubgraph, not_nil_iff_lt_length, not_nil_of_isCycle_cons, not_nil_of_ne, nil_nil, nil_takeUntil, nil_reverse, darts_eq_nil, IsCycle.not_nil, edges_eq_nil, head_darts_eq_firstDart
|
cons' 📖 | CompOp | — |
darts 📖 | CompOp | 44 mathmath: lastDart_eq_getLast_darts, exists_boundary_dart, darts_take, head_darts_fst, mem_darts_iff_infix_support, darts_copy, darts_concat, firstDart_eq_head_darts, darts_injective, isSubwalk_toWalk_iff_mem_darts, mem_darts_reverse, firstDart_mem_darts, darts_map, darts_toPath_subset, getLast_darts_snd, isChain_dartAdj_darts, darts_nodup_of_support_nodup, map_fst_darts_append, darts_drop, darts_reverse, IsSubwalk.darts_subset, darts_cons, getLast_darts_eq_lastDart, isSubwalk_iff_darts_isInfix, length_darts, IsSubwalk.darts_isInfix, chain'_dartAdj_darts, darts_append, darts_nil, chain_dartAdj_darts, darts_bypass_subset, toDeleteEdges_cons, mem_darts_iff_fst_snd_infix_support, map_snd_darts, cons_map_snd_darts, darts_eq_nil, lastDart_mem_darts, darts_dropUntil_subset, darts_takeUntil_subset, isChain_dartAdj_cons_darts, map_fst_darts, head_darts_eq_firstDart, rotate_darts, isSubwalk_toWalk_adj_iff_mem_darts
|
edgeSet 📖 | CompOp | 15 mathmath: edgeSet_toSubgraph, IsEulerian.edgeSet_eq, edgeSet_reverse, edgeSet_nil, edgeSet_concat, edgeSet_copy, mem_edgeSet, toSubgraph_le_iff, edgeSet_map, edgeSet_append, edgeSet_cons, coe_edges_toFinset, edgeSet_mapLe_eq_edgeSet, IsTrail.isEulerian_iff, edgeSet_transfer
|
edges 📖 | CompOp | 61 mathmath: isEulerian_iff, edges_copy, edges_take, edges_mapLe_eq_edges, edges_eq_zipWith_support, edges_concat, edges_nodup_of_support_nodup, head_edges_eq_mk_start_snd, SimpleGraph.IsAcyclic.isPath_iff_isChain, IsTrail.edges_nodup, rotate_edges, cons_isCycle_iff, isTrail_def, edges_transfer, mk_start_snd_eq_head_edges, SimpleGraph.reachable_delete_edges_iff_exists_walk, transfer_transfer, SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle, SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges, edges_takeUntil_subset, IsTrail.even_countP_edges_iff, IsTrail.count_edges_le_one, edges_dropUntil_subset, edges_nil, mem_edgeSet, exists_mem_edges_of_not_reachable_deleteEdges, infix_support_iff_mem_edges, mem_edges_of_not_reachable_deleteEdges, SimpleGraph.Path.notMem_edges_of_loop, edges_cycleBypass_subset, mk_penultimate_end_eq_getLast_edges, SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem, edges_cons, edges_bypass_subset, IsTrail.not_mem_edges_of_not_reachable, isSubwalk_toWalk_iff_mem_edges, adj_toSubgraph_iff_mem_edges, mk_penultimate_end_mem_edges, mem_support_iff_exists_mem_edges_of_not_nil, SimpleGraph.Path.mk'_mem_edges_singleton, edges_drop, cons_isTrail_iff, edges_append, edges_injective, edges_toPath_subset, edges_reverse, IsSubwalk.edges_subset, count_edges_takeUntil_le_one, getLast_edges_eq_mk_penultimate_end, IsSubwalk.edges_isInfix, coe_edges_toFinset, IsTrail.disjoint_edges_takeUntil_dropUntil, IsEulerian.mem_edges_iff, isTrail_cons, edges_map, mem_edges_toSubgraph, mk_start_snd_mem_edges, SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem, length_edges, mem_support_iff_exists_mem_edges, edges_eq_nil
|
instDecidableNil 📖 | CompOp | — |
instInhabited 📖 | CompOp | 1 mathmath: default_def
|
length 📖 | CompOp | 89 mathmath: SimpleGraph.exists_girth_eq_length, SimpleGraph.set_walk_length_zero_eq_of_ne, length_tail_add_one, SimpleGraph.walkLengthTwoEquivCommonNeighbors_symm_apply_coe, toSubgraph_adj_iff, edist_le, nil_iff_length_eq, length_bypass_le, exists_isTrail_forall_isTrail_length_le_length, SimpleGraph.card_set_walk_length_eq, SimpleGraph.exists_egirth_eq_length, SimpleGraph.is3Clique_iff_exists_cycle_length_three, getVert_reverse, IsHamiltonianCycle.length_eq, length_takeUntil_lt, length_takeUntil_le, getVert_append, SimpleGraph.Connected.exists_walk_length_eq_dist, SimpleGraph.dist_eq_sInf, length_support, SimpleGraph.set_walk_self_length_zero_eq, SimpleGraph.mem_finsetWalkLength_iff, length_reverseAux, SimpleGraph.adjMatrix_pow_apply_eq_card_walk, isCycle_iff_isPath_tail_and_le_length, IsPath.getVert_injOn, darts_getElem_eq_getVert, isHamiltonian_iff_isPath_and_length_eq, nil_drop_iff, SimpleGraph.coe_finsetWalkLength_eq, take_length, SimpleGraph.Connected.exists_path_of_dist, SimpleGraph.set_walk_length_toFinset_eq, length_boxProd, SimpleGraph.edist_eq_sInf, SimpleGraph.dist_le, SimpleGraph.Connected.exists_walk_length_eq_edist, length_le_of_isSubwalk, length_map, length_concat, SimpleGraph.girth_le_length, exists_isPath_forall_isPath_length_le_length, IsPath.getVert_injOn_iff, SimpleGraph.set_walk_length_succ_eq, length_append, exists_length_eq_zero_iff, length_transfer, length_dropUntil, length_copy, not_nil_iff_lt_length, drop_length, length_nil, length_darts, getVert_length, IsHamiltonian.length_eq, support_getElem_length, isHamiltonianCycle_iff_isCycle_and_length_eq, length_takeUntil, SimpleGraph.egirth_le_length, IsCycle.getVert_injOn', SimpleGraph.Reachable.exists_walk_length_eq_dist, SimpleGraph.cycleGraph_EulerianCircuit_length, support_getElem_length_sub_one_eq_penultimate, SimpleGraph.two_colorable_iff_forall_loop_even, SimpleGraph.exists_walk_of_edist_ne_top, SimpleGraph.mem_finsetWalkLengthLT_iff, length_reverse, SimpleGraph.exists_walk_of_edist_eq_coe, length_cons, IsCycle.three_le_length, IsTrail.length_le_card_edgeFinset, SimpleGraph.Coloring.odd_length_iff_not_congr, SimpleGraph.le_egirth, SimpleGraph.edist_le, SimpleGraph.Reachable.exists_walk_length_eq_edist, SimpleGraph.coe_finsetWalkLengthLT_eq, IsPath.length_lt, SimpleGraph.exists_walk_of_dist_ne_zero, SimpleGraph.walkLengthTwoEquivCommonNeighbors_apply_coe, drop_support_eq_support_drop_min, exists_length_eq_one_iff, length_eq_zero_iff, SimpleGraph.Coloring.even_length_iff_congr, SimpleGraph.Reachable.exists_path_of_dist, length_edges, mem_support_iff_exists_getVert, IsCycle.getVert_injOn, getVert_length_takeUntil, length_dropUntil_le
|
nil' 📖 | CompOp | — |
notNilRec 📖 | CompOp | 1 mathmath: notNilRec_cons
|
support 📖 | CompOp | 116 mathmath: penultimate_mem_dropLast_support, mem_support_of_adj_toSubgraph, support_eq_cons, IsHamiltonian.getVertEquiv_apply, nil_iff_support_eq, edges_eq_zipWith_support, support_toPath_subset, mem_darts_iff_infix_support, getVert_eq_support_getElem?, range_getVert_eq_range_support_getElem, head_support, isCycle_def, snd_darts_getElem, support_cons, start_mem_support, map_induce_induceHomOfLE, support_transfer, isPath_def, end_mem_tail_support, support_copy, IsHamiltonian.support_toFinset, isSubwalk_nil_iff_mem_support, length_support, IsCycle.count_support, mem_verts_toSubgraph, isHamiltonian_iff_support_get_bijective, getVert_mem_support, subset_support_append_left, IsHamiltonian.getVertEquiv_symm_apply, support_getElem_zero, getVert_mem_tail_support, IsTrail.not_mem_edges_of_not_isEdgeReachable_two, getLast_support, IsHamiltonian.mem_support, map_fst_darts_append, support_nil, isChain_adj_cons_support, getVert_eq_support_getElem, infix_support_iff_mem_edges, IsHamiltonian.supportGetEquiv_apply, IsHamiltonianCycle.support_count_of_ne, coe_support_append, IsHamiltonian.supportGetEquiv_symm_apply_val, end_mem_support, mem_support_iff_exists_append, mem_tail_support_append_iff, snd_eq_support_getElem_one, dart_fst_mem_support_of_mem_darts, support_concat, mem_support_nil_iff, IsPath.disjoint_support_of_append, getVert_comp_val_eq_get_support, map_mapToSubgraph_eq_induce_id, subset_support_append_right, SimpleGraph.Path.nodup_support, snd_mem_tail_support, chain'_adj_support, support_nonempty, mem_support_iff, end_mem_tail_support_of_ne, support_tail, toSubgraph_le_induce_support, IsPath.mem_support_iff_exists_append, support_tail_of_not_nil, support_subset_support_concat, IsHamiltonianCycle.mem_support, support_append_eq_support_dropLast_append, verts_toSubgraph, support_append, snd_mem_support_of_mem_edges, mem_support_iff_exists_mem_edges_of_not_nil, support_getElem_length, support_induce, isChain_adj_support, support_getElem_length_sub_one_eq_penultimate, IsPath.support_nodup, dart_snd_mem_support_of_mem_darts, support_eq_concat, IsCycle.support_nodup, nodup_tail_support_reverse, IsPath.isHamiltonian_iff, chain_adj_support, cons_isPath_iff, mem_darts_iff_fst_snd_infix_support, fst_darts_getElem, support_bypass_subset, support_map, isPath_iff_injective_get_support, cons_support_tail, support_reverse, map_snd_darts, cons_map_snd_darts, support_injective, IsTrail.not_mem_support_of_subsingleton_neighborSet, isSubwalk_iff_support_isInfix, tail_support_append, support_mapLe_eq_support, support_subset_support_cons, mem_support_of_mem_edges, IsHamiltonianCycle.count_support_self, getVert_eq_getD_support, IsTrail.not_mem_support_of_not_reachable, drop_support_eq_support_drop_min, fst_mem_support_of_mem_edges, isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one, mem_support_iff_exists_mem_edges, coe_support_append', IsHamiltonian.length_support, connected_induce_support, mem_support_append_iff, mem_support_iff_exists_getVert, coe_support, concat_isPath_iff, IsSubwalk.support_subset, take_support_eq_support_take_succ, map_fst_darts
|