| Metric | Count |
|---|
DefinitionssimpleGraph, comap, comp, complEquiv, completeGraph, induce, map, mapEdgeSet, mapNeighborSet, refl, spanningCoe, toHom, comap, comp, id, instUniqueOfIsEmpty, mapDart, mapEdgeSet, mapNeighborSet, ofLE, HomClass, comap, comp, completeGraph, map, mapEdgeSet, mapNeighborSet, refl, toEmbedding, toHom, comap, completeMultipartiteGraph, induce, induceHom, induceHomOfLE, induceUnivIso, instDecidableComapAdj, instDecidableMapAdj, map, overFin, overFinIso, spanningCoe, «term_→g_», «term_↪g_», «term_≃g_» | 45 |
TheoremssimpleGraph_apply, simpleGraph_refl, simpleGraph_trans, symm_simpleGraph, apply_mem_neighborSet_iff, coe_comp, coe_completeGraph, coe_toHom, comap_apply, mapEdgeSet_apply, mapNeighborSet_apply_coe, map_adj_iff, map_apply, map_mem_edgeSet_iff, apply_mem_neighborSet, coe_comp, coe_id, coe_ofLE, comap_apply, injective_of_top_hom, instFinite, instIsEmptyOfForall, instSubsingletonOfForall, mapDart_apply, injective, mapEdgeSet_coe, mapNeighborSet_coe, map_adj, map_mem_edgeSet, ofLE_apply, induce, apply_mem_neighborSet_iff, card_eq, coe_comp, comap_apply, comap_symm_apply, mapEdgeSet_apply, mapEdgeSet_symm_apply, mapNeighborSet_apply_coe, mapNeighborSet_symm_apply_coe, map_adj_iff, map_apply, map_mem_edgeSet_iff, map_symm_apply, symm_toHom_comp_toHom, toEmbedding_completeGraph, toHom_comp_symm_toHom, coe_induceHom, comap_adj, comap_bot, comap_comap, comap_id, comap_map_eq, comap_monotone, comap_surjective, comap_symm, comap_top, edgeSet_map, induceHomOfLE_apply, induceHomOfLE_toHom, induceHom_comp, induceHom_id, induceHom_injective, induceUnivIso_apply, induceUnivIso_symm_apply_coe, induce_adj, induce_singleton_eq_top, induce_spanningCoe, induce_top, le_comap_of_subsingleton, leftInverse_comap_map, map_adj, map_adj_apply, map_comap_le, map_id, map_injective, map_le_iff_le_comap, map_le_of_subsingleton, map_map, map_monotone, map_symm, spanningCoe_induce_le, support_map | 83 |
| Total | 128 |
| Name | Category | Theorems |
|---|
HomClass 📖 | MathDef | — |
comap 📖 | CompOp | 21 mathmath: leftInverse_comap_map, comap_bot, comap_symm, comap_surjective, Hom.comap_apply, map_symm, le_comap_of_subsingleton, comap_adj, IsAcyclic.of_comap, Iso.comap_apply, comap_id, comap_comap, Embedding.comap_apply, Equiv.simpleGraph_apply, comap_map_eq, map_le_iff_le_comap, map_comap_le, comap_top, locallyLinear_comap, Iso.comap_symm_apply, comap_monotone
|
completeMultipartiteGraph 📖 | CompOp | 10 mathmath: completeMultipartiteGraph.not_cliqueFree_of_le_card, completeMultipartiteGraph.topEmbedding_apply_fst, cliqueFree_completeMultipartiteGraph, completeMultipartiteGraph.not_cliqueFree_of_le_enatCard, completeMultipartiteGraph.chromaticNumber, completeMultipartiteGraph.topEmbedding_apply_snd, completeMultipartiteGraph.colorable, completeMultipartiteGraph.isCompleteMultipartite, isCompleteMultipartite_iff, completeMultipartiteGraph.not_cliqueFree_of_infinite
|
induce 📖 | CompOp | 48 mathmath: ConnectedComponent.maximal_connected_induce_supp, coe_induceHom, spanningCoe_induce_top, IsAcyclic.induce, isClique_iff_induce_eq, map_edgeFinset_induce_of_support_subset, IsCompleteBetween.induce, Preconnected.induce_of_degree_eq_one, induce_eq_coe_induce_top, Walk.map_induce_induceHomOfLE, induceUnivIso_apply, extend_finset_to_connected, ConnectedComponent.maximal_connected_induce_iff, Walk.map_mapToSubgraph_eq_induce, induceHom_id, induce_deleteIncidenceSet_of_notMem, Walk.induce_cons, Connected.exists_preconnected_induce_compl_singleton_of_finite, induce_pair_connected_of_adj, spanningCoe_induce_le, map_neighborFinset_induce_of_neighborSet_subset, degree_induce_support, Connected.induce_compl_singleton_of_degree_eq_one, induceHom_injective, induceHomOfLE_apply, Walk.map_mapToSubgraph_eq_induce_id, map_neighborFinset_induce, induce_singleton_eq_top, preconnected_induce_iff, connected_induce_iff, degree_induce_of_neighborSet_subset, induceHom_comp, Walk.support_induce, Walk.induce_nil, induceUnivIso_symm_apply_coe, card_edgeFinset_induce_support, Walk.map_induce, degree_induce_of_support_subset, induceHomOfLE_toHom, induce_adj, Connected.exists_connected_induce_compl_singleton_of_finite_nontrivial, induce_spanningCoe, Subgraph.Connected.induce_verts, card_edgeFinset_induce_of_support_subset, induce_top, map_edgeFinset_induce, Walk.connected_induce_support, card_edgeFinset_induce_compl_singleton
|
induceHom 📖 | CompOp | 5 mathmath: coe_induceHom, induceHom_id, induceHom_injective, induceHom_comp, induceHomOfLE_toHom
|
induceHomOfLE 📖 | CompOp | 3 mathmath: Walk.map_induce_induceHomOfLE, induceHomOfLE_apply, induceHomOfLE_toHom
|
induceUnivIso 📖 | CompOp | 2 mathmath: induceUnivIso_apply, induceUnivIso_symm_apply_coe
|
instDecidableComapAdj 📖 | CompOp | 13 mathmath: map_edgeFinset_induce_of_support_subset, neighborFinset_completeEquipartiteGraph, degree_completeEquipartiteGraph, map_neighborFinset_induce_of_neighborSet_subset, degree_induce_support, map_neighborFinset_induce, degree_induce_of_neighborSet_subset, card_edgeFinset_induce_support, card_edgeFinset_completeEquipartiteGraph, degree_induce_of_support_subset, card_edgeFinset_induce_of_support_subset, map_edgeFinset_induce, card_edgeFinset_induce_compl_singleton
|
instDecidableMapAdj 📖 | CompOp | 4 mathmath: card_edgeFinset_map, edgeFinset_map, cliqueFinset_map_of_equiv, cliqueFinset_map
|
map 📖 | CompOp | 37 mathmath: isClique_map_image_iff, leftInverse_comap_map, card_edgeFinset_map, map_le_of_subsingleton, Iso.map_symm_apply, edgeFinset_map, cliqueSet_map_of_equiv, isClique_map_finset_iff, IsNClique.map, comap_symm, cliqueFinset_map_of_equiv, map_adj, cliqueSet_map, isClique_map_finset_iff_of_nontrivial, map_adj_apply, IsClique.finsetMap, cliqueFinset_map, map_symm, map_injective, map_id, map_monotone, isClique_map_iff_of_nontrivial, LocallyLinear.map, isNClique_map_iff, Embedding.map_apply, Colorable.map, edgeSet_map, map_map, support_map, EdgeDisjointTriangles.map, comap_map_eq, cliqueFree_map_iff, map_le_iff_le_comap, isClique_map_iff, map_comap_le, Iso.map_apply, IsClique.map
|
overFin 📖 | CompOp | — |
overFinIso 📖 | CompOp | — |
spanningCoe 📖 | CompOp | 7 mathmath: spanningCoe_induce_top, IsCycles.toSimpleGraph, ConnectedComponent.adj_spanningCoe_toSimpleGraph, spanningCoe_induce_le, ConnectedComponent.spanningCoe_toSubgraph, Subgraph.spanningCoe_coe, induce_spanningCoe
|
«term_→g_» 📖 | CompOp | — |
«term_↪g_» 📖 | CompOp | — |
«term_≃g_» 📖 | CompOp | — |