| Metric | Count |
|---|
DefinitionsSimpleGraph, adjDecidable, adjDecidable, adjDecidable, IsCompleteBetween, IsSubgraph, adjDecidable, adjDecidable, adjDecidable, commonNeighbors, completeAtomicBooleanAlgebra, completeGraph, decidableMemCommonNeighbors, decidableMemEdgeSet, decidableMemIncidenceSet, distribLattice, edgeSet, edgeSetEmbedding, emptyGraph, fintypeEdgeSet, fintypeEdgeSetBot, fintypeEdgeSetInf, fintypeEdgeSetSdiff, fintypeEdgeSetSup, fromEdgeSet, fromRel, incidenceSet, incidenceSetEquivNeighborSet, infSet, instCompl, instDecidableRelAdjFromEdgeSetOfDecidablePredSym2MemSetOfDecidableEq, instFintypeElemSym2EdgeSetFromEdgeSetOfDecidableEq, instInhabited, instLE, instMax, instMin, instPartialOrder, mk', neighborSet, memDecidable, otherVertexOfIncident, sdiff, supSet, support, uniqueOfSubsingleton, aesop_graph, aesop_graph?, aesop_graph_nonterminal, completeBipartiteGraph, instDecidableRelAdjFromRelOfDecidableEq, instFintypeSimpleGraphOfDecidableEq | 51 |
Theoremsne, ne', disjoint, adj_comm, adj_congr_of_sym2, adj_iff_exists_edge, adj_iff_exists_edge_coe, adj_incidenceSet_inter, adj_inj, adj_injective, adj_of_mem_incidenceSet, adj_symm, bot_adj, card_neighborSet_union_compl_neighborSet, commonNeighbors_eq, commonNeighbors_subset_neighborSet_left, commonNeighbors_subset_neighborSet_right, commonNeighbors_symm, commonNeighbors_top_eq, compl_adj, compl_neighborSet_disjoint, completeGraph_eq_top, default_def, disjoint_edgeSet, disjoint_fromEdgeSet, disjoint_left, edgeSet_bot, edgeSet_eq_empty, edgeSet_eq_iff, edgeSet_fromEdgeSet, edgeSet_inf, edgeSet_inj, edgeSet_injective, edgeSet_mono, edgeSet_nonempty, edgeSet_sdiff, edgeSet_sdiff_sdiff_isDiag, edgeSet_ssubset_edgeSet, edgeSet_strict_mono, edgeSet_subset_compl_diagSet, edgeSet_subset_edgeSet, edgeSet_subset_setOf_not_isDiag, edgeSet_sup, edgeSet_top, edge_mem_incidenceSet_iff, edge_other_incident_set, edge_other_ne, emptyGraph_eq_bot, eq_bot_iff_forall_not_adj, eq_top_iff_forall_ne_adj, ext, ext_iff, fromEdgeSet_adj, fromEdgeSet_disjoint, fromEdgeSet_edgeSet, fromEdgeSet_empty, fromEdgeSet_inter, fromEdgeSet_le, fromEdgeSet_mono, fromEdgeSet_not_isDiag, fromEdgeSet_sdiff, fromEdgeSet_union, fromEdgeSet_univ, fromRel_adj, iInf_adj, iInf_adj_of_nonempty, iSup_adj, incidenceSetEquivNeighborSet_apply_coe, incidenceSetEquivNeighborSet_symm_apply_coe, incidenceSet_inter_incidenceSet_of_adj, incidenceSet_inter_incidenceSet_of_not_adj, incidenceSet_inter_incidenceSet_subset, incidenceSet_subset, incidence_other_neighbor_edge, incidence_other_prop, inf_adj, instFinite, instNontrivial, irrefl, isCompleteBetween_comm, isSubgraph_eq_le, le_iff_adj, loopless, mem_commonNeighbors, mem_edgeSet, mem_incidenceSet, mem_incidence_iff_neighbor, mem_neighborSet, mem_support, mk'_apply_adj, mk'_mem_incidenceSet_iff, mk'_mem_incidenceSet_left_iff, mk'_mem_incidenceSet_right_iff, ne_bot_iff_exists_adj, ne_of_adj, ne_of_adj_of_not_adj, ne_top_iff_exists_not_adj, neighborSet_compl, neighborSet_subset_support, neighborSet_union_compl_neighborSet_eq, nontrivial_iff, notMem_commonNeighbors_left, notMem_commonNeighbors_right, notMem_neighborSet_self, not_isDiag_of_mem_edgeSet, not_mem_edgeSet_of_isDiag, sInf_adj, sInf_adj_of_nonempty, sSup_adj, sdiff_adj, subsingleton_iff, sup_adj, support_bot, support_eq_bot_iff, support_mono, support_of_subsingleton, support_top_of_nontrivial, symm_adj, top_adj, not_mem_edgeSet, completeBipartiteGraph_adj | 121 |
| Total | 172 |
| Name | Category | Theorems |
|---|
IsCompleteBetween 📖 | MathDef | 2 mathmath: completeBipartiteGraph_isContained_iff, isCompleteBetween_comm
|
IsSubgraph 📖 | MathDef | 1 mathmath: isSubgraph_eq_le
|
commonNeighbors 📖 | CompOp | 19 mathmath: walkLengthTwoEquivCommonNeighbors_symm_apply_coe, card_commonNeighbors_le_degree_left, IsSRGWith.card_neighborFinset_union_eq, Adj.card_commonNeighbors_lt_degree, mem_commonNeighbors, notMem_commonNeighbors_left, card_commonNeighbors_le_degree_right, commonNeighbors_eq, commonNeighbors_symm, commonNeighbors_subset_neighborSet_right, card_commonNeighbors_lt_card_verts, IsSRGWith.of_adj, IsSRGWith.card_commonNeighbors_eq_of_adj_compl, card_commonNeighbors_top, commonNeighbors_top_eq, walkLengthTwoEquivCommonNeighbors_apply_coe, IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl, notMem_commonNeighbors_right, commonNeighbors_subset_neighborSet_left
|
completeAtomicBooleanAlgebra 📖 | CompOp | 140 mathmath: locallyLinear_bot, cliqueSet_bot, killCopies_bot, TopEdgeLabeling.labelGraph_adj, cliqueFree_two, eccent_bot, copyCount_bot, turanGraph_eq_top, bot_not_connected, isExtremal_top_free_iff_isTuranMaximal, toTopEdgeLabeling_labelGraph_compl, edgeFinset_top, isClique_iff_induce_eq, bot_not_preconnected, Copy.topEmbedding_apply, UnitDistEmbedding.bot_p, cycleGraph_one_eq_bot, edgeDisjointTriangles_bot, emptyGraph_eq_bot, chromaticNumber_top, center_bot, edgeSet_top, completeMultipartiteGraph.topEmbedding_apply_fst, deleteEdges_univ, girth_bot, support_top_of_nontrivial, neighborFinset_completeEquipartiteGraph, toTopEdgeLabeling_get, cycleGraph_two_eq_top, IsSRGWith.top, degree_completeEquipartiteGraph, free_bot, edist_top, cycleGraph_three_eq_top, disjoint_edge, edgeSet_bot, disjoint_edgeFinset, edge_self_eq_bot, cliqueFree_bot, Digraph.toSimpleGraphStrict_top, Subgraph.spanningCoe_bot, disjoint_edgeSet, preconnected_top, fromEdgeSet_not_isDiag, ConnectedComponent.top_supp_eq_univ, preconnected_bot, chromaticNumber_eq_card_iff, egirth_bot, support_eq_bot_iff, EdgeLabeling.pairwise_disjoint_labelGraph, extremalNumber_top, isVertexCover_bot, dist_top_of_ne, top_adj, maxDegree_bot_eq_zero, card_edgeFinset_top_eq_card_choose_two, fromEdgeSet_univ, vertexCoverNum_eq_zero, isExtremal_top_free_turanGraph, ediam_top, not_connected_bot, default_def, Digraph.toSimpleGraphInclusive_bot, top_isIndContained_iff_top_isContained, ediam_eq_one, diam_eq_one, toTopEdgeLabeling_labelGraph, IsContained.bot, edist_bot, bot_isContained_iff_card_le, dist_bot, EdgeLabeling.pairwiseDisjoint_univ_labelGraph, diam_bot, nonempty_dart_top, turanGraph_zero, fromEdgeSet_disjoint, support_bot, fromEdgeSet_empty, connected_bot_iff, induce_singleton_eq_top, pathGraph_two_eq_top, cycleGraph_one_eq_top, lineGraph_bot, reachable_bot, isNClique_map_copy_top, bot_preconnected_iff_subsingleton, bot_adj, isClique_bot_iff, diam_top, isClique_range_copy_top, eq_bot_iff_forall_not_adj, edgeFinset_bot, eq_top_iff_forall_eccent_eq_one, TopEdgeLabeling.labelGraph_toTopEdgeLabeling, completeGraph_eq_top, center_top, completeEquipartiteGraph_eq_bot_iff, disjoint_left, not_isHamiltonian_bot_of_card_ne_one, completeMultipartiteGraph.topEmbedding_apply_snd, chromaticNumber_top_eq_top_of_infinite, top_preconnected, card_commonNeighbors_top, eq_top_iff_forall_ne_adj, edgeFinset_eq_empty, Digraph.toSimpleGraphInclusive_top, disjoint_fromEdgeSet, bot_degree, bot_isCompleteMultipartite, radius_top, Digraph.toSimpleGraphStrict_bot, commonNeighbors_top_eq, minDegree_bot_eq_zero, preconnected_bot_iff_subsingleton, card_edgeFinset_completeEquipartiteGraph, radius_bot, eq_top_of_chromaticNumber_eq_card, edgeSet_eq_empty, not_preconnected_bot, killCopies_def, IsRegularOfDegree.top, isAcyclic_bot, Hom.injective_of_top_hom, isNClique_bot_iff, bot_preconnected, ediam_bot, card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph, edist_top_of_ne, cliqueFree_iff_top_free, cycleGraph_zero_eq_bot, chromaticNumber_eq_one_iff, bot_strongly_regular, card_topEdgeLabeling, cycleGraph_zero_eq_top, isVertexCover_empty, edist_bot_of_ne, dist_top, eccent_top, chromaticNumber_bot, Subgraph.coe_bot
|
completeGraph 📖 | CompOp | 27 mathmath: connected_top, Coloring.mem_colorClass, card_le_chromaticNumber_iff_forall_surjective, vertexCoverNum_top, cliqueFree_iff, le_chromaticNumber_iff_forall_surjective, top_connected, connected_top_iff, Coloring.injective_comp_of_pairwise_adj, colorable_iff_exists_bdd_nat_coloring, coe_recolorOfEmbedding, coe_recolorOfEquiv, complete_graph_degree, not_cliqueFree_iff, completeGraph_eq_top, Coloring.surjOn_of_card_le_isClique, Embedding.coe_completeGraph, Coloring.odd_length_iff_not_congr, reachable_top, Iso.toEmbedding_completeGraph, chromaticNumber_eq_iff_forall_surjective, Coloring.mem_colorClasses, induce_top, coe_recolorOfCardLE, Coloring.even_length_iff_congr, comap_top, chromaticNumber_eq_card_iff_forall_surjective
|
decidableMemCommonNeighbors 📖 | CompOp | 9 mathmath: card_commonNeighbors_le_degree_left, IsSRGWith.card_neighborFinset_union_eq, Adj.card_commonNeighbors_lt_degree, card_commonNeighbors_le_degree_right, card_commonNeighbors_lt_card_verts, IsSRGWith.of_adj, IsSRGWith.card_commonNeighbors_eq_of_adj_compl, card_commonNeighbors_top, IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl
|
decidableMemEdgeSet 📖 | CompOp | — |
decidableMemIncidenceSet 📖 | CompOp | 1 mathmath: incMatrix_apply'
|
distribLattice 📖 | CompOp | — |
edgeSet 📖 | CompOp | 73 mathmath: not_mem_edgeSet_of_isDiag, edgeSet_fromEdgeSet, fromEdgeSet_edgeSet, adj_iff_exists_edge_coe, deleteEdges_edgeSet, Walk.IsEulerian.edgeSet_eq, Subgraph.image_coe_edgeSet_coe, coe_edgeFinset, edgeSet_top, edgeSet_ssubset_edgeSet, edgeSet_replaceVertex_of_adj, Embedding.map_mem_edgeSet_iff, edge_edgeSet_of_ne, edgeSet_eq_iff, edgeSet_bot, edgeSet_inf, edgeSet_subset_edgeSet, Subgraph.edgeSet_top, Subgraph.edgeSet_iInf, disjoint_edgeSet, Iso.map_mem_edgeSet_iff, edgeSet_deleteIncidenceSet, Hom.mapEdgeSet_coe, isTree_iff_connected_and_card, vertexCoverNum_le_encard_edgeSet, edge_mem_incidenceSet_iff, edgeSet_nonempty, Hom.mapEdgeSet.injective, Subgraph.edgeSet_sInf, edgeSet_sdiff_sdiff_isDiag, Connected.card_vert_le_card_edgeSet_add_one, fromEdgeSet_le, edgeSet_fromEdgeSet_incidenceSet, edgeSet_inj, edgeSet_strict_mono, fromEdgeSet_disjoint, Subgraph.edgeSet_subset, lineGraph_bot, deleteEdges_eq_inter_edgeSet, edgeSet_mono, mem_edgeFinset, incMatrix_transpose_mul_diag, Dart.edge_mem, edgeSet_subset_setOf_not_isDiag, EdgeLabeling.get_eq, Subgraph.edgeSet_coe, edgeSet_map, Sym2.IsDiag.not_mem_edgeSet, disjoint_fromEdgeSet, lineGraph_adj_iff_exists, edgeSet_univ_card, edgeSet_sup, Embedding.mapEdgeSet_apply, Walk.IsEulerian.mem_edges_iff, Iso.mapEdgeSet_apply, edgeSet_replaceVertex_of_not_adj, edgeSet_eq_empty, edgeSet_deleteEdges, Walk.IsTrail.isEulerian_iff, card_edgeSet, edgeSet_injective, edgeSet_sdiff, edgeSet_subset_compl_diagSet, mem_edgeSet, Walk.edges_subset_edgeSet, deleteEdges_sdiff_eq_of_le, deleteEdges_eq_self, adj_iff_exists_edge, incidenceSet_subset, EdgeLabeling.labelGraph_adj, isBridge_iff_mem_and_forall_cycle_notMem, edgeFinset_card, Iso.mapEdgeSet_symm_apply
|
edgeSetEmbedding 📖 | CompOp | — |
emptyGraph 📖 | CompOp | 3 mathmath: emptyGraph_eq_bot, comap_bot, vertexCoverNum_bot
|
fintypeEdgeSet 📖 | CompOp | 52 mathmath: 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, card_edgeFinset_sup_edge, edgeFinset_top, map_edgeFinset_induce_of_support_subset, extremalNumber_le_iff_of_nonneg, card_edgeFinset_map, farFromTriangleFree_iff, 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, card_edgeFinset_le_extremalNumber, farFromTriangleFree.le_card_sub_card, isExtremal_free_iff, card_edgeFinset_turanGraph_add, edgeFinset_replaceVertex_of_not_adj, extremalNumber_top, card_edgeFinset_deleteIncidenceSet_le_extremalNumber, card_edgeFinset_top_eq_card_choose_two, dart_card_eq_twice_card_edges, extremalNumber_of_fintypeCard_eq, edgeFinset_deleteIncidenceSet_eq_filter, card_edgeFinset_replaceVertex_of_not_adj, card_edgeFinset_replaceVertex_of_adj, sum_degrees_support_eq_twice_card_edges, extremalNumber_le_iff, card_edgeFinset_deleteIncidenceSet, lt_extremalNumber_iff, lt_extremalNumber_iff_of_nonneg, disjoint_sdiff_neighborFinset_image, regularityReduced_edges_card_aux, triangle_removal, card_edgeFinset_turanGraph, card_edgeFinset_induce_support, card_edgeFinset_completeEquipartiteGraph, edgeFinset_sup_edge, CliqueFree.card_edgeFinset_le, card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph, card_edgeFinset_induce_of_support_subset, map_edgeFinset_induce, card_topEdgeLabeling, mul_card_edgeFinset_turanGraph_le, isBipartiteWith_sum_degrees_eq_twice_card_edges, card_edgeFinset_induce_compl_singleton
|
fintypeEdgeSetBot 📖 | CompOp | 1 mathmath: edgeFinset_bot
|
fintypeEdgeSetInf 📖 | CompOp | 1 mathmath: edgeFinset_inf
|
fintypeEdgeSetSdiff 📖 | CompOp | 1 mathmath: edgeFinset_sdiff
|
fintypeEdgeSetSup 📖 | CompOp | — |
fromEdgeSet 📖 | CompOp | 23 mathmath: fromEdgeSet_mono, fromEdgeSet_inter, edgeSet_fromEdgeSet, fromEdgeSet_edgeSet, Subgraph.spanningCoe_subgraphOfAdj, deleteEdges_fromEdgeSet, reachable_delete_edges_iff_exists_walk, edgeSet_eq_iff, adj_and_reachable_delete_edges_iff_exists_cycle, fromEdgeSet_not_isDiag, fromEdgeSet_adj, reachable_fromEdgeSet_eq_reflTransGen_toRel, fromEdgeSet_sdiff, fromEdgeSet_univ, fromEdgeSet_le, edgeSet_fromEdgeSet_incidenceSet, isBridge_iff, fromEdgeSet_disjoint, fromEdgeSet_empty, isAcyclic_add_edge_iff_of_not_reachable, disjoint_fromEdgeSet, fromEdgeSet_union, reachable_fromEdgeSet_fromRel_eq_reflTransGen
|
fromRel 📖 | CompOp | 1 mathmath: fromRel_adj
|
incidenceSet 📖 | CompOp | 27 mathmath: mem_incidenceSet, incidenceSetEquivNeighborSet_apply_coe, incidenceSet_inter_incidenceSet_of_adj, incMatrix_apply_mul_incMatrix_apply, incidenceSet_inter_incidenceSet_of_not_adj, adj_incidenceSet_inter, card_incidenceSet_eq_degree, mem_incidenceFinset, edgeSet_replaceVertex_of_adj, incMatrix_apply', edgeSet_deleteIncidenceSet, edge_mem_incidenceSet_iff, incidenceSetEquivNeighborSet_symm_apply_coe, incMatrix_apply_eq_one_iff, mem_incidence_iff_neighbor, incidenceSet_inter_incidenceSet_subset, edgeSet_fromEdgeSet_incidenceSet, coe_incidenceFinset, Subgraph.incidenceSet_subset_incidenceSet, mk'_mem_incidenceSet_left_iff, edgeSet_replaceVertex_of_not_adj, mk'_mem_incidenceSet_iff, incMatrix_apply, incidence_other_neighbor_edge, incidenceSet_subset, mk'_mem_incidenceSet_right_iff, incMatrix_apply_eq_zero_iff
|
incidenceSetEquivNeighborSet 📖 | CompOp | 2 mathmath: incidenceSetEquivNeighborSet_apply_coe, incidenceSetEquivNeighborSet_symm_apply_coe
|
infSet 📖 | CompOp | 4 mathmath: sInf_adj, iInf_adj, iInf_adj_of_nonempty, sInf_adj_of_nonempty
|
instCompl 📖 | CompOp | 33 mathmath: isNClique_compl, toTopEdgeLabeling_labelGraph_compl, card_interedges_add_card_interedges_compl, cliqueNum_compl, reachable_or_reachable_compl, IsRegularOfDegree.compl, neighborFinset_compl, isMaximalIndepSet_compl, neighborSet_union_compl_neighborSet_eq, neighborSet_compl, compl_isIndContained_compl, connected_or_connected_compl, IsSRGWith.matrix_eq, isIndepSet_compl, compl_adj, compl_neighborSet_disjoint, Matrix.IsAdjMatrix.toGraph_compl_eq, IsSRGWith.compl_is_regular, isMaximalClique_compl, IsIndContained.compl, isClique_compl, isNIndepSet_compl, degree_compl, isMaximumClique_compl, IsSRGWith.compl, connected_or_preconnected_compl, reachable_or_compl_adj, edgeDensity_add_edgeDensity_compl, card_neighborSet_union_compl_neighborSet, indepSetFree_compl, isMaximumIndepSet_compl, cliqueFree_compl, indepNum_compl
|
instDecidableRelAdjFromEdgeSetOfDecidablePredSym2MemSetOfDecidableEq 📖 | CompOp | — |
instFintypeElemSym2EdgeSetFromEdgeSetOfDecidableEq 📖 | CompOp | — |
instInhabited 📖 | CompOp | 1 mathmath: default_def
|
instLE 📖 | CompOp | 35 mathmath: fromEdgeSet_mono, deleteIncidenceSet_le, IsExtremal.le_iff_eq, killCopies_le_left, map_le_of_subsingleton, isTree_iff_minimal_connected, between_le, EdgeLabeling.labelGraph_le, regularityReduced_mono, Subgraph.spanningCoe_le, edgeSet_subset_edgeSet, exists_maximal_isMatchingFree, le_iff_adj, spanningCoe_induce_le, Connected.exists_isTree_le, Subgraph.coe_deleteEdges_le, deleteEdges_anti, fromEdgeSet_le, le_comap_of_subsingleton, Subgraph.spanningCoe_sup_edge_le, regularityReduced_le, maximal_isAcyclic_iff_isTree, Subgraph.spanningCoe_deleteEdges_le, isSubgraph_eq_le, edgeFinset_subset_edgeFinset, regularityReduced_anti, triangle_removal, pathGraph_le_cycleGraph, Subgraph.spanningCoe_le_of_le, edge_le_iff, map_le_iff_le_comap, map_comap_le, exists_isAcyclic_reachable_eq_le, Digraph.toSimpleGraphStrict_subgraph_toSimpleGraphInclusive, deleteEdges_le
|
instMax 📖 | CompOp | 24 mathmath: card_edgeFinset_sup_edge, sup_edge_self, CliqueFree.sup_edge, lt_sup_edge, Subgraph.IsPerfectMatching.isAlternating_symmDiff_left, sup_adj, Reachable.sum_sup_edge, edgeFinset_sup, isClique_sup_edge_of_ne_sdiff, deleteEdges_sup, Subgraph.IsPerfectMatching.symmDiff_isCycles, Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge, Subgraph.IsPerfectMatching.symmDiff_of_isAlternating, isAcyclic_add_edge_iff_of_not_reachable, Subgraph.sup_spanningCoe, Preconnected.sum_sup_edge, isClique_sup_edge_of_ne_iff, sup_edge_of_adj, edgeFinset_sup_edge, edgeSet_sup, fromEdgeSet_union, IsAlternating.sup_edge, Subgraph.IsPerfectMatching.isAlternating_symmDiff_right, Connected.sum_sup_edge
|
instMin 📖 | CompOp | 4 mathmath: fromEdgeSet_inter, edgeSet_inf, edgeFinset_inf, inf_adj
|
instPartialOrder 📖 | CompOp | 18 mathmath: lt_sup_edge, edgeSet_ssubset_edgeSet, disjoint_edge, disjoint_edgeFinset, disjoint_edgeSet, Digraph.toSimpleGraphStrict_mono, EdgeLabeling.pairwise_disjoint_labelGraph, EdgeLabeling.pairwiseDisjoint_univ_labelGraph, fromEdgeSet_disjoint, map_monotone, Digraph.toSimpleGraphInclusive_mono, disjoint_left, egirth_anti, disjoint_fromEdgeSet, Copy.ofLE_refl, Copy.ofLE_comp, comap_monotone, edgeFinset_ssubset_edgeFinset
|
mk' 📖 | CompOp | 1 mathmath: mk'_apply_adj
|
neighborSet 📖 | CompOp | 47 mathmath: incidenceSetEquivNeighborSet_apply_coe, isBipartiteWith_neighborSet_disjoint, Subgraph.neighborSet_iInf, Embedding.apply_mem_neighborSet_iff, neighborSet_subset_between_union, card_neighborSet_eq_degree, Embedding.mapNeighborSet_apply_coe, notMem_neighborSet_self, edgeSet_replaceVertex_of_adj, neighborSet_union_compl_neighborSet_eq, neighborSet_compl, Iso.apply_mem_neighborSet_iff, degree_pos_iff_nonempty, incidenceSetEquivNeighborSet_symm_apply_coe, mem_neighborSet, commonNeighbors_eq, neighborSet_subset_between_union_compl, incidence_other_prop, mem_incidence_iff_neighbor, CliqueFreeOn.of_succ, dartOfNeighborSet_injective, compl_neighborSet_disjoint, dart_fst_fiber, Iso.mapNeighborSet_apply_coe, commonNeighbors_subset_neighborSet_right, isBipartiteWith_neighborSet_disjoint', Subgraph.neighborSet_top, isBipartiteWith_neighborSet', Subgraph.neighborSet_eq_of_equiv, Hom.mapNeighborSet_coe, isBipartiteWith_neighborSet, isBipartiteWith_neighborSet_subset', neighborSet_boxProd, dartOfNeighborSet_toProd, Iso.mapNeighborSet_symm_apply_coe, neighborSet_subset_support, cycleGraph_neighborSet, Subgraph.neighborSet_sInf, edgeSet_replaceVertex_of_not_adj, isIndepSet_neighborSet_of_triangleFree, card_neighborSet_union_compl_neighborSet, coe_neighborFinset, neighborSet_completeEquipartiteGraph, neighborFinset_def, isBipartiteWith_neighborSet_subset, Subgraph.neighborSet_subset, commonNeighbors_subset_neighborSet_left
|
otherVertexOfIncident 📖 | CompOp | 4 mathmath: incidenceSetEquivNeighborSet_apply_coe, incidence_other_prop, edge_other_incident_set, incidence_other_neighbor_edge
|
sdiff 📖 | CompOp | 14 mathmath: edgeFinset_sdiff, deleteEdges_edgeSet, IsCycles.reachable_sdiff_toSubgraph_spanningCoe, Subgraph.IsPerfectMatching.isAlternating_symmDiff_left, reachable_delete_edges_iff_exists_walk, adj_and_reachable_delete_edges_iff_exists_cycle, fromEdgeSet_sdiff, isBridge_iff, Subgraph.IsPerfectMatching.symmDiff_isCycles, sdiff_adj, Subgraph.IsPerfectMatching.symmDiff_of_isAlternating, sdiff_edge, edgeSet_sdiff, Subgraph.IsPerfectMatching.isAlternating_symmDiff_right
|
supSet 📖 | CompOp | 4 mathmath: EdgeLabeling.iSup_labelGraph, sSup_adj, isAcyclic_sSup_of_isAcyclic_directedOn, iSup_adj
|
support 📖 | CompOp | 18 mathmath: mem_support, Preconnected.support_eq_univ, degree_eq_zero_iff_notMem_support, support_of_subsingleton, support_top_of_nontrivial, isBipartiteWith_support_subset, support_eq_bot_iff, mem_support_of_reachable, degree_induce_support, support_bot, sum_degrees_support_eq_twice_card_edges, support_mono, degree_pos_iff_mem_support, neighborSet_subset_support, support_map, card_edgeFinset_induce_support, mem_support_of_mem_walk_support, support_deleteIncidenceSet_subset
|
uniqueOfSubsingleton 📖 | CompOp | — |