| Name | Category | Theorems |
|---|
IsRegularOfDegree 📖 | MathDef | 3 mathmath: IsSRGWith.regular, IsSRGWith.compl_is_regular, IsRegularOfDegree.top
|
degree 📖 | CompOp | 70 mathmath: Preconnected.degree_pos_of_nontrivial, degree_le_maxDegree, isBipartiteWith_degree_le', sum_degrees_eq_twice_card_edges, sum_incMatrix_apply, degree_lt_card_verts, degree_eq_zero_iff_notMem_support, Adj.degree_pos_left, card_incidenceSet_eq_degree, card_commonNeighbors_le_degree_left, card_neighborSet_eq_degree, dotProduct_mulVec_degMatrix, isBipartiteWith_sum_degrees_eq_card_edges, Subgraph.coe_degree, Adj.card_commonNeighbors_lt_degree, degree_completeEquipartiteGraph, isBipartiteWith_sum_degrees_eq_card_edges', degree_pos_iff_exists_adj, exists_minimal_degree_vertex, even_card_odd_degree_vertices, cycleGraph_degree_three_le, Adj.degree_pos_right, degree_pos_iff_nonempty, Walk.IsEulerian.even_degree_iff, card_commonNeighbors_le_degree_right, degree_induce_support, card_neighborSet_toSubgraph, incMatrix_mul_transpose, adjMatrix_mulVec_const_apply, degree_le_between_add, card_edgeFinset_replaceVertex_of_not_adj, lapMatrix_mulVec_apply, card_edgeFinset_replaceVertex_of_adj, card_neighborFinset_eq_degree, Subgraph.degree_le, degree_toSubgraph, IsTuranMaximal.degree_eq_of_not_adj, sum_degrees_support_eq_twice_card_edges, complete_graph_degree, dart_card_eq_sum_degrees, isBipartiteWith_degree_le, exists_maximal_degree_vertex, degree_induce_of_neighborSet_subset, incMatrix_mul_transpose_diag, dart_fst_fiber_card_eq_degree, Iso.degree_eq, card_edgeFinset_deleteIncidenceSet, degree_compl, degree_eq_sum_if_adj, degree_pos_iff_mem_support, card_incidenceFinset_eq_degree, bot_degree, degree_le_of_le, degree_le_between_add_compl, degree_le_card_edgeFinset, adjMatrix_mul_self_apply_self, IsTree.exists_vert_degree_one_of_nontrivial, degMatrix_mulVec_apply, degree_induce_of_support_subset, IsRegularOfDegree.degree_eq, cycleGraph_degree_two_le, IsTuranMaximal.degree_eq_card_sub_part_card, Subgraph.degree_spanningCoe, Walk.IsEulerian.card_odd_degree, degree_eq_zero_of_subsingleton, minDegree_le_degree, degree_boxProd, degree_eq_one_iff_existsUnique_adj, isBipartiteWith_sum_degrees_eq, isBipartiteWith_sum_degrees_eq_twice_card_edges
|
edgeFinset 📖 | CompOp | 81 mathmath: edgeFinset_mono, deleteFar_iff, EdgeDisjointTriangles.card_edgeFinset_le, edgeFinset_subset_sym2_of_support_subset, DeleteFar.le_card_sub_card, two_mul_card_edgeFinset, sum_degrees_eq_twice_card_edges, edgeFinset_sdiff, card_edgeFinset_sup_edge, edgeFinset_inj, edgeFinset_top, map_edgeFinset_induce_of_support_subset, extremalNumber_le_iff_of_nonneg, card_edgeFinset_le_card_choose_two, incidenceFinset_eq_filter, card_edgeFinset_map, farFromTriangleFree_iff, coe_edgeFinset, edgeFinset_deleteIncidenceSet_eq_sdiff, isBipartiteWith_sum_degrees_eq_card_edges, edgeFinset_map, card_edgeFinset_of_isExtremal_free, isBipartiteWith_sum_degrees_eq_card_edges', edgeFinset_replaceVertex_of_adj, LocallyLinear.card_edgeFinset, edgeFinset_nonempty, card_edgeFinset_le_extremalNumber, farFromTriangleFree.le_card_sub_card, disjoint_edgeFinset, isExtremal_free_iff, card_edgeFinset_turanGraph_add, le_card_edgeFinset_killCopies_add_copyCount, edgeFinset_replaceVertex_of_not_adj, Iso.card_edgeFinset_eq, incidenceFinset_subset, extremalNumber_top, edgeFinset_sup, card_edgeFinset_deleteIncidenceSet_le_extremalNumber, card_edgeFinset_top_eq_card_choose_two, dart_card_eq_twice_card_edges, extremalNumber_of_fintypeCard_eq, DeleteFar.le_card_edgeFinset, edgeFinset_deleteIncidenceSet_eq_filter, edgeFinset_strict_mono, card_edgeFinset_replaceVertex_of_not_adj, le_card_edgeFinset_killCopies, card_edgeFinset_replaceVertex_of_adj, sum_degrees_support_eq_twice_card_edges, mem_edgeFinset, edgeFinset_bot, extremalNumber_le_iff, card_edgeFinset_deleteIncidenceSet, lt_extremalNumber_iff, edgeFinset_subset_edgeFinset, lt_extremalNumber_iff_of_nonneg, Walk.IsEulerian.edgesFinset_eq, edgeFinset_eq_empty, disjoint_sdiff_neighborFinset_image, regularityReduced_edges_card_aux, degree_le_card_edgeFinset, triangle_removal, card_edgeFinset_turanGraph, edgeSet_univ_card, card_edgeFinset_induce_support, card_edgeFinset_completeEquipartiteGraph, Walk.IsTrail.length_le_card_edgeFinset, edgeFinset_sup_edge, card_toFinset_mem_edgeFinset, CliqueFree.card_edgeFinset_le, card_edgeSet, card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph, card_edgeFinset_induce_of_support_subset, edgeFinset_deleteEdges, edgeFinset_inf, map_edgeFinset_induce, edgeFinset_card, mul_card_edgeFinset_turanGraph_le, IsTree.card_edgeFinset, isBipartiteWith_sum_degrees_eq_twice_card_edges, edgeFinset_ssubset_edgeFinset, card_edgeFinset_induce_compl_singleton
|
incidenceFinset 📖 | CompOp | 9 mathmath: incidenceFinset_eq_filter, edgeFinset_deleteIncidenceSet_eq_sdiff, mem_incidenceFinset, edgeFinset_replaceVertex_of_adj, edgeFinset_replaceVertex_of_not_adj, incidenceFinset_subset, coe_incidenceFinset, card_incidenceFinset_eq_degree, disjoint_sdiff_neighborFinset_image
|
incidenceSetFintype 📖 | CompOp | 1 mathmath: card_incidenceSet_eq_degree
|
instDecidablePredMemSetSupport 📖 | CompOp | 4 mathmath: degree_induce_support, card_support_deleteIncidenceSet, sum_degrees_support_eq_twice_card_edges, card_edgeFinset_induce_support
|
maxDegree 📖 | CompOp | 8 mathmath: degree_le_maxDegree, Iso.maxDegree_eq, maxDegree_bot_eq_zero, exists_maximal_degree_vertex, maxDegree_le_of_forall_degree_le, minDegree_le_maxDegree, maxDegree_of_isEmpty, maxDegree_lt_card_verts
|
minDegree 📖 | CompOp | 12 mathmath: minDegree_lt_card, minDegree_of_isEmpty, exists_minimal_degree_vertex, le_minDegree_of_forall_le_degree, IsTree.minDegree_eq_one_of_nontrivial, Iso.minDegree_eq, Preconnected.minDegree_pos_of_nontrivial, minDegree_bot_eq_zero, minDegree_le_maxDegree, IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ, minDegree_le_minDegree, minDegree_le_degree
|
neighborFinset 📖 | CompOp | 39 mathmath: adjMatrix_mulVec_apply, isBipartiteWith_neighborFinset_disjoint, IsSRGWith.card_neighborFinset_union_eq, mul_adjMatrix_apply, notMem_neighborFinset_self, neighborFinset_completeEquipartiteGraph, neighborFinset_compl, neighborFinset_disjoint_singleton, edgeFinset_replaceVertex_of_adj, neighborFinset_subset_between_union, isBipartiteWith_neighborFinset, edgeFinset_replaceVertex_of_not_adj, neighborFinset_subset_between_union_compl, neighborFinset_boxProd, isBipartiteWith_neighborFinset_subset, isBipartiteWith_neighborFinset_disjoint', dotProduct_adjMatrix, map_neighborFinset_induce_of_neighborSet_subset, lapMatrix_mulVec_apply, cycleGraph_neighborFinset, card_neighborFinset_eq_degree, isBipartiteWith_bipartiteBelow, map_neighborFinset_induce, mem_neighborFinset, sdiff_compl_neighborFinset_inter_eq, IsSRGWith.card_neighborFinset_union_of_not_adj, adjMatrix_mul_apply, IsSRGWith.card_neighborFinset_union_of_adj, adjMatrix_vecMul_apply, disjoint_sdiff_neighborFinset_image, compl_neighborFinset_sdiff_inter_eq, adjMatrix_dotProduct, neighborFinset_eq_filter, coe_neighborFinset, isBipartiteWith_bipartiteAbove, isBipartiteWith_neighborFinset_subset', singleton_disjoint_neighborFinset, neighborFinset_def, isBipartiteWith_neighborFinset'
|
neighborSetFintype 📖 | CompOp | 69 mathmath: degree_le_maxDegree, adjMatrix_mulVec_apply, sum_degrees_eq_twice_card_edges, degree_lt_card_verts, card_commonNeighbors_le_degree_left, IsSRGWith.card_neighborFinset_union_eq, mul_adjMatrix_apply, edgeFinset_deleteIncidenceSet_eq_sdiff, neighborFinset_completeEquipartiteGraph, dotProduct_mulVec_degMatrix, isBipartiteWith_sum_degrees_eq_card_edges, neighborFinset_compl, Adj.card_commonNeighbors_lt_degree, degree_completeEquipartiteGraph, isBipartiteWith_sum_degrees_eq_card_edges', reachable_iff_exists_finsetWalkLength_nonempty, edgeFinset_replaceVertex_of_adj, neighborFinset_subset_between_union, exists_minimal_degree_vertex, edgeFinset_replaceVertex_of_not_adj, neighborFinset_subset_between_union_compl, even_card_odd_degree_vertices, cycleGraph_degree_three_le, Walk.IsEulerian.even_degree_iff, card_commonNeighbors_le_degree_right, adjMatrix_pow_apply_eq_card_walk, dotProduct_adjMatrix, IsSRGWith.regular, map_neighborFinset_induce_of_neighborSet_subset, degree_induce_support, adjMatrix_mulVec_const_apply, degree_le_between_add, card_edgeFinset_replaceVertex_of_not_adj, lapMatrix_mulVec_apply, dart_fst_fiber, IsSRGWith.compl_is_regular, cycleGraph_neighborFinset, card_edgeFinset_replaceVertex_of_adj, map_neighborFinset_induce, sdiff_compl_neighborFinset_inter_eq, IsSRGWith.card_neighborFinset_union_of_not_adj, IsTuranMaximal.degree_eq_of_not_adj, sum_degrees_support_eq_twice_card_edges, complete_graph_degree, dart_card_eq_sum_degrees, exists_maximal_degree_vertex, adjMatrix_mul_apply, degree_induce_of_neighborSet_subset, IsSRGWith.card_neighborFinset_union_of_adj, dart_fst_fiber_card_eq_degree, card_edgeFinset_deleteIncidenceSet, degree_eq_sum_if_adj, adjMatrix_vecMul_apply, disjoint_sdiff_neighborFinset_image, bot_degree, degree_le_between_add_compl, adjMatrix_mul_self_apply_self, IsTree.exists_vert_degree_one_of_nontrivial, compl_neighborFinset_sdiff_inter_eq, adjMatrix_dotProduct, neighborFinset_eq_filter, degMatrix_mulVec_apply, degree_induce_of_support_subset, cycleGraph_degree_two_le, IsTuranMaximal.degree_eq_card_sub_part_card, IsRegularOfDegree.top, Walk.IsEulerian.card_odd_degree, minDegree_le_degree, isBipartiteWith_sum_degrees_eq_twice_card_edges
|