| Metric | Count |
|---|
DefinitionsSubgraph, IsInduced, IsSpanning, botEquiv, botIso, coeDeleteVertsIso, coeFiniteAt, coeInduceIso, coeNeighborSetEquiv, coeSubgraph, comap, completelyDistribLatticeMinimalAxioms, copy, degree, deleteEdges, deleteVerts, distribLattice, edgeSet, finiteAt, finiteAtOfSubgraph, hom, incidenceSet, inclusion, induce, instBot, instBoundedOrder, instCompletelyDistribLattice, instDecidableRelElemVertsAdjCoeOfAdj, instDecidableRel_deleteVerts_adj, instDecidableRel_induce_adj, instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet, instFintypeOfDecidableEqOfDecidableRelAdj, instInfSet, instMax, instMin, instPartialOrder, instSupSet, instTop, map, neighborSet, decidablePred, restrict, spanningCoe, spanningCoeEquivCoeOfSpanning, spanningHom, subgraphInhabited, support, topEquiv, topIso, vert, verts, instUniqueElemVertsSingletonSubgraph, singletonSubgraph, subgraphOfAdj, toSubgraph | 55 |
TheoremsedgeSet, adj_sub, adj_sub', fst_mem, ne, of_spanningCoe, snd_mem, adj, induce_top_verts, top, card_verts, verts_eq_univ, adj_comm, adj_congr_of_sym2, adj_iff_of_neighborSet_equiv, adj_sub, adj_symm, coeSubgraph_adj, coeSubgraph_injective, coeSubgraph_le, coeSubgraph_restrict_eq, coe_adj, coe_adj_sub, coe_bot, coe_degree, coe_deleteEdges_eq, coe_deleteEdges_le, coe_hom, comap_adj, comap_equiv_top, comap_monotone, comap_verts, copy_eq, degree_eq_one_iff_existsUnique_adj, degree_eq_one_iff_unique_adj, degree_eq_zero_of_subsingleton, degree_le, degree_le', degree_of_notMem_verts, degree_pos_iff_exists_adj, degree_spanningCoe, deleteEdges_adj, deleteEdges_coe_eq, deleteEdges_deleteEdges, deleteEdges_empty_eq, deleteEdges_inter_edgeSet_left_eq, deleteEdges_inter_edgeSet_right_eq, deleteEdges_le, deleteEdges_le_of_le, deleteEdges_spanningCoe_eq, deleteEdges_verts, deleteVerts_adj, deleteVerts_anti, deleteVerts_deleteVerts, deleteVerts_empty, deleteVerts_inter_verts_left_eq, deleteVerts_inter_verts_set_right_eq, deleteVerts_le, deleteVerts_mono, deleteVerts_mono', deleteVerts_verts, edgeSet_bot, edgeSet_coe, edgeSet_iInf, edgeSet_iSup, edgeSet_inf, edgeSet_map, edgeSet_mono, edgeSet_sInf, edgeSet_sSup, edgeSet_subset, edgeSet_sup, edgeSet_top, edge_vert, eq_bot_iff_verts_eq_empty, ext, ext_iff, finset_card_neighborSet_eq_degree, hom_apply, hom_injective, iInf_adj, iInf_adj_of_nonempty, iSup_adj, image_coe_edgeSet_coe, incidenceSet_subset, incidenceSet_subset_incidenceSet, injective, inclusion_apply_coe, induce_adj, induce_empty, induce_mono, induce_mono_left, induce_mono_right, induce_self_verts, induce_verts, inf_adj, instFinite, isInduced_iff_exists_eq_induce_top, isSpanning_iff, le_induce_top_verts, le_induce_union, le_induce_union_left, le_induce_union_right, loopless, map_adj, map_comp, map_hom_top, map_id, map_iso_top, map_le_iff_le_comap, map_mono, map_monotone, map_sup, map_verts, mem_edgeSet, mem_neighborSet, mem_of_adj_spanningCoe, mem_support, mem_verts_of_mem_edge, ne_bot_iff_nonempty_verts, neighborSet_bot, neighborSet_eq_of_equiv, neighborSet_iInf, neighborSet_iSup, neighborSet_inf, neighborSet_sInf, neighborSet_sSup, neighborSet_subset, neighborSet_subset_of_subgraph, neighborSet_subset_verts, neighborSet_sup, neighborSet_top, nontrivial_verts_of_degree_ne_zero, not_bot_adj, restrict_adj, restrict_coeSubgraph, sInf_adj, sInf_adj_of_nonempty, sSup_adj, singletonSubgraph_eq_induce, spanningCoeEquivCoeOfSpanning_apply_coe, spanningCoeEquivCoeOfSpanning_symm_apply, spanningCoe_adj, spanningCoe_bot, spanningCoe_coe, spanningCoe_deleteEdges_le, spanningCoe_inj, spanningCoe_le, spanningCoe_le_of_le, spanningCoe_subgraphOfAdj, spanningCoe_top, spanningHom_apply, spanningHom_injective, subgraphInhabited_default, subgraphOfAdj_eq_induce, sup_adj, sup_spanningCoe, support_mono, support_subset_verts, top_adj, verts_bot, verts_coeSubgraph, verts_iInf, verts_iSup, verts_inf, verts_mono, verts_monotone, verts_sInf, verts_sSup, verts_spanningCoe_injective, verts_sup, verts_top, card_neighborSet_toSubgraph, degree_toSubgraph, edgeSet_singletonSubgraph, edgeSet_subgraphOfAdj, eq_singletonSubgraph_iff_verts_eq, induce_eq_coe_induce_top, map_singletonSubgraph, map_subgraphOfAdj, neighborSet_fst_subgraphOfAdj, neighborSet_singletonSubgraph, neighborSet_snd_subgraphOfAdj, neighborSet_subgraphOfAdj, neighborSet_subgraphOfAdj_of_ne_of_ne, neighborSet_subgraphOfAdj_subset, nonempty_singletonSubgraph_verts, nonempty_subgraphOfAdj_verts, singletonSubgraph_adj, singletonSubgraph_fst_le_subgraphOfAdj, singletonSubgraph_le_iff, singletonSubgraph_snd_le_subgraphOfAdj, singletonSubgraph_verts, spanningCoe_induce_top, subgraphOfAdj_adj, subgraphOfAdj_le_of_adj, subgraphOfAdj_symm, subgraphOfAdj_verts, support_subgraphOfAdj, isSpanning, toSubgraph_adj, toSubgraph_verts | 202 |
| Total | 257 |
| Name | Category | Theorems |
|---|
IsInduced 📖 | MathDef | 4 mathmath: SimpleGraph.IsIndContained.exists_iso_subgraph, isInduced_iff_exists_eq_induce_top, SimpleGraph.isIndContained_iff_exists_iso_subgraph, IsInduced.top
|
IsSpanning 📖 | MathDef | 2 mathmath: SimpleGraph.toSubgraph.isSpanning, isSpanning_iff
|
botEquiv 📖 | CompOp | — |
botIso 📖 | CompOp | — |
coeDeleteVertsIso 📖 | CompOp | — |
coeFiniteAt 📖 | CompOp | — |
coeInduceIso 📖 | CompOp | — |
coeNeighborSetEquiv 📖 | CompOp | — |
coeSubgraph 📖 | CompOp | 10 mathmath: coeSubgraph_injective, verts_coeSubgraph, coeSubgraph_le, IsMatching.coeSubgraph, Preconnected.coeSubgraph, SimpleGraph.Reachable.coe_coeSubgraph, coeSubgraph_adj, coeSubgraph_restrict_eq, restrict_coeSubgraph, Connected.coeSubgraph
|
comap 📖 | CompOp | 5 mathmath: comap_verts, comap_equiv_top, comap_monotone, map_le_iff_le_comap, comap_adj
|
completelyDistribLatticeMinimalAxioms 📖 | CompOp | — |
copy 📖 | CompOp | 1 mathmath: copy_eq
|
degree 📖 | CompOp | 14 mathmath: degree_eq_one_iff_unique_adj, coe_degree, degree_of_notMem_verts, Preconnected.degree_zero_iff, isPerfectMatching_iff_forall_degree, degree_eq_one_iff_existsUnique_adj, degree_eq_zero_of_subsingleton, isMatching_iff_forall_degree, degree_le, SimpleGraph.degree_toSubgraph, degree_le', finset_card_neighborSet_eq_degree, degree_pos_iff_exists_adj, degree_spanningCoe
|
deleteEdges 📖 | CompOp | 13 mathmath: deleteEdges_spanningCoe_eq, deleteEdges_empty_eq, deleteEdges_coe_eq, coe_deleteEdges_le, deleteEdges_inter_edgeSet_right_eq, deleteEdges_le_of_le, deleteEdges_inter_edgeSet_left_eq, deleteEdges_adj, spanningCoe_deleteEdges_le, deleteEdges_le, deleteEdges_verts, deleteEdges_deleteEdges, coe_deleteEdges_eq
|
deleteVerts 📖 | CompOp | 11 mathmath: deleteVerts_anti, deleteVerts_deleteVerts, deleteVerts_mono', deleteVerts_inter_verts_set_right_eq, SimpleGraph.ConnectedComponent.odd_matches_node_outside, deleteVerts_empty, deleteVerts_le, deleteVerts_verts, deleteVerts_mono, deleteVerts_adj, deleteVerts_inter_verts_left_eq
|
distribLattice 📖 | CompOp | — |
edgeSet 📖 | CompOp | 26 mathmath: SimpleGraph.Walk.edgeSet_toSubgraph, IsMatching.toEdge_eq_of_adj, image_coe_edgeSet_coe, edgeSet_bot, mem_edgeSet, edgeSet_top, edgeSet_iInf, IsMatching.toEdge.surjective, SimpleGraph.edgeSet_subgraphOfAdj, edgeSet_map, deleteEdges_inter_edgeSet_right_eq, edgeSet_mono, edgeSet_sInf, edgeSet_sSup, deleteEdges_inter_edgeSet_left_eq, SimpleGraph.Walk.toSubgraph_le_iff, edgeSet_iSup, edgeSet_subset, edgeSet_sup, incidenceSet_subset, edgeSet_coe, Disjoint.edgeSet, SimpleGraph.killCopies_def, SimpleGraph.Walk.mem_edges_toSubgraph, edgeSet_inf, SimpleGraph.edgeSet_singletonSubgraph
|
finiteAt 📖 | CompOp | — |
finiteAtOfSubgraph 📖 | CompOp | — |
hom 📖 | CompOp | 5 mathmath: map_hom_top, SimpleGraph.Walk.map_mapToSubgraph_hom, hom_injective, hom_apply, coe_hom
|
incidenceSet 📖 | CompOp | 2 mathmath: incidenceSet_subset_incidenceSet, incidenceSet_subset
|
inclusion 📖 | CompOp | 2 mathmath: inclusion_apply_coe, inclusion.injective
|
induce 📖 | CompOp | 27 mathmath: le_induce_union_right, IsPerfectMatching.induce_connectedComponent_isMatching, SimpleGraph.spanningCoe_induce_top, Connected.adj_union, induce_adj, top_induce_pair_connected_of_adj, SimpleGraph.induce_eq_coe_induce_top, le_induce_top_verts, IsMatching.induce_connectedComponent, le_induce_union_left, induce_empty, connected_induce_top_sup, induce_verts, isInduced_iff_exists_eq_induce_top, SimpleGraph.preconnected_induce_iff, SimpleGraph.Walk.toSubgraph_le_induce_support, SimpleGraph.isIndepSet_induce, SimpleGraph.connected_induce_iff, singletonSubgraph_eq_induce, subgraphOfAdj_eq_induce, le_induce_union, SimpleGraph.isNIndepSet_induce, IsInduced.induce_top_verts, induce_self_verts, induce_mono, induce_mono_right, induce_mono_left
|
instBot 📖 | CompOp | 11 mathmath: neighborSet_bot, edgeSet_bot, induce_empty, spanningCoe_bot, isAcyclic_coe_bot, SimpleGraph.Finsubgraph.coe_bot, not_bot_adj, subgraphInhabited_default, eq_bot_iff_verts_eq_empty, verts_bot, coe_bot
|
instBoundedOrder 📖 | CompOp | — |
instCompletelyDistribLattice 📖 | CompOp | 4 mathmath: SimpleGraph.Finsubgraph.coe_hnot, SimpleGraph.Finsubgraph.coe_sdiff, SimpleGraph.Finsubgraph.coe_himp, SimpleGraph.Finsubgraph.coe_compl
|
instDecidableRelElemVertsAdjCoeOfAdj 📖 | CompOp | — |
instDecidableRel_deleteVerts_adj 📖 | CompOp | — |
instDecidableRel_induce_adj 📖 | CompOp | — |
instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet 📖 | CompOp | — |
instFintypeOfDecidableEqOfDecidableRelAdj 📖 | CompOp | — |
instInfSet 📖 | CompOp | 12 mathmath: neighborSet_iInf, edgeSet_iInf, SimpleGraph.Finsubgraph.coe_iInf, iInf_adj, sInf_adj, edgeSet_sInf, sInf_adj_of_nonempty, verts_iInf, iInf_adj_of_nonempty, neighborSet_sInf, SimpleGraph.Finsubgraph.coe_sInf, verts_sInf
|
instMax 📖 | CompOp | 14 mathmath: sup_adj, Connected.adj_union, verts_sup, Connected.sup, IsMatching.sup, connected_induce_top_sup, connected_sup, map_sup, SimpleGraph.Finsubgraph.coe_sup, SimpleGraph.Walk.toSubgraph_append, edgeSet_sup, neighborSet_sup, sup_spanningCoe, le_induce_union
|
instMin 📖 | CompOp | 6 mathmath: inf_adj, neighborSet_inf, verts_inf, SimpleGraph.Finsubgraph.coe_inf, coeSubgraph_restrict_eq, edgeSet_inf
|
instPartialOrder 📖 | CompOp | 28 mathmath: le_induce_union_right, deleteVerts_anti, SimpleGraph.singletonSubgraph_fst_le_subgraphOfAdj, coeSubgraph_le, SimpleGraph.singletonSubgraph_le_iff, le_induce_top_verts, SimpleGraph.singletonSubgraph_snd_le_subgraphOfAdj, SimpleGraph.Walk.toSubgraph_bypass_le_toSubgraph, le_induce_union_left, SimpleGraph.ConnectedComponent.maximal_connected_toSubgraph, SimpleGraph.Finsubgraph.coe_bot, verts_monotone, deleteEdges_le_of_le, connected_iff_forall_exists_walk_subgraph, SimpleGraph.Walk.toSubgraph_le_iff, deleteVerts_le, map_monotone, SimpleGraph.Walk.toSubgraph_le_induce_support, SimpleGraph.subgraphOfAdj_le_of_adj, preconnected_iff_forall_exists_walk_subgraph, SimpleGraph.ConnectedComponent.maximal_subgraph_connected_iff, deleteEdges_le, le_induce_union, SimpleGraph.singletonFinsubgraph_le_adj_left, comap_monotone, map_le_iff_le_comap, induce_mono_right, SimpleGraph.singletonFinsubgraph_le_adj_right
|
instSupSet 📖 | CompOp | 11 mathmath: SimpleGraph.Finsubgraph.coe_sSup, neighborSet_sSup, neighborSet_iSup, sSup_adj, edgeSet_sSup, edgeSet_iSup, SimpleGraph.Finsubgraph.coe_iSup, verts_iSup, iSup_adj, verts_sSup, IsMatching.iSup
|
instTop 📖 | CompOp | 28 mathmath: deleteVerts_mono', SimpleGraph.Finsubgraph.coe_top, SimpleGraph.spanningCoe_induce_top, Connected.adj_union, top_induce_pair_connected_of_adj, SimpleGraph.induce_eq_coe_induce_top, le_induce_top_verts, verts_top, SimpleGraph.ConnectedComponent.odd_matches_node_outside, edgeSet_top, map_hom_top, connected_induce_top_sup, comap_equiv_top, map_iso_top, isInduced_iff_exists_eq_induce_top, neighborSet_top, SimpleGraph.preconnected_induce_iff, SimpleGraph.Walk.toSubgraph_le_induce_support, SimpleGraph.isIndepSet_induce, SimpleGraph.connected_induce_iff, IsPerfectMatching.symmDiff_of_isAlternating, singletonSubgraph_eq_induce, subgraphOfAdj_eq_induce, IsInduced.top, top_adj, SimpleGraph.isNIndepSet_induce, IsInduced.induce_top_verts, spanningCoe_top
|
map 📖 | CompOp | 20 mathmath: SimpleGraph.map_singletonSubgraph, Preconnected.map, IsMatching.map, Connected.map, map_comp, map_hom_top, edgeSet_map, map_verts, map_adj, map_iso_top, IsMatching.map_ofLE, map_sup, map_monotone, map_id, SimpleGraph.Reachable.coe_subgraphMap, map_le_iff_le_comap, map_mono, SimpleGraph.map_subgraphOfAdj, SimpleGraph.Walk.toSubgraph_map, Iso.isMatching_map
|
neighborSet 📖 | CompOp | 29 mathmath: SimpleGraph.neighborSet_subgraphOfAdj_subset, neighborSet_bot, neighborSet_sSup, neighborSet_iInf, SimpleGraph.Walk.IsPath.ncard_neighborSet_toSubgraph_internal_eq_two, neighborSet_subset_verts, neighborSet_iSup, SimpleGraph.neighborSet_fst_subgraphOfAdj, SimpleGraph.Walk.IsCycle.ncard_neighborSet_toSubgraph_eq_two, SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_internal, SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_startpoint, SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_endpoint, SimpleGraph.neighborSet_snd_subgraphOfAdj, neighborSet_inf, SimpleGraph.card_neighborSet_toSubgraph, SimpleGraph.Walk.finite_neighborSet_toSubgraph, mem_neighborSet, SimpleGraph.neighborSet_subgraphOfAdj_of_ne_of_ne, neighborSet_top, neighborSet_eq_of_equiv, neighborSet_sup, SimpleGraph.neighborSet_singletonSubgraph, finset_card_neighborSet_eq_degree, neighborSet_sInf, SimpleGraph.neighborSet_subgraphOfAdj, SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_endpoint, SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_internal, neighborSet_subset, neighborSet_subset_of_subgraph
|
restrict 📖 | CompOp | 3 mathmath: coeSubgraph_restrict_eq, restrict_coeSubgraph, restrict_adj
|
spanningCoe 📖 | CompOp | 27 mathmath: SimpleGraph.spanningCoe_induce_top, verts_spanningCoe_injective, SimpleGraph.Walk.IsCycle.isCycles_spanningCoe_toSubgraph, spanningCoe_subgraphOfAdj, SimpleGraph.IsAlternating.spanningCoe, spanningHom_injective, deleteEdges_spanningCoe_eq, SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoe, IsPerfectMatching.isAlternating_symmDiff_left, spanningCoe_inj, spanningCoe_le, spanningCoe_bot, spanningCoeEquivCoeOfSpanning_apply_coe, SimpleGraph.ConnectedComponent.spanningCoe_toSubgraph, IsPerfectMatching.symmDiff_isCycles, spanningCoe_sup_edge_le, SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge, spanningCoeEquivCoeOfSpanning_symm_apply, spanningCoe_deleteEdges_le, spanningHom_apply, sup_spanningCoe, spanningCoe_coe, spanningCoe_top, spanningCoe_adj, spanningCoe_le_of_le, degree_spanningCoe, IsPerfectMatching.isAlternating_symmDiff_right
|
spanningCoeEquivCoeOfSpanning 📖 | CompOp | 2 mathmath: spanningCoeEquivCoeOfSpanning_apply_coe, spanningCoeEquivCoeOfSpanning_symm_apply
|
spanningHom 📖 | CompOp | 2 mathmath: spanningHom_injective, spanningHom_apply
|
subgraphInhabited 📖 | CompOp | 1 mathmath: subgraphInhabited_default
|
support 📖 | CompOp | 5 mathmath: SimpleGraph.support_subgraphOfAdj, support_subset_verts, support_mono, IsMatching.support_eq_verts, mem_support
|
topEquiv 📖 | CompOp | — |
topIso 📖 | CompOp | — |
vert 📖 | CompOp | 1 mathmath: SimpleGraph.Reachable.coe_coeSubgraph
|
verts 📖 | CompOp | 127 mathmath: SimpleGraph.Finsubgraph.coe_sSup, edge_vert, deleteVerts_mono', SimpleGraph.deleteUniversalVerts_verts, SimpleGraph.Finsubgraph.coe_top, coeSubgraph_injective, verts_coeSubgraph, IsInduced.adj, neighborSet_subset_verts, SimpleGraph.Finsubgraph.coe_hnot, verts_spanningCoe_injective, verts_sup, SimpleGraph.Finsubgraph.coe_sdiff, SimpleGraph.singletonSubgraph_le_iff, SimpleGraph.isContained_iff_exists_iso_subgraph, le_induce_top_verts, image_coe_edgeSet_coe, comap_verts, IsMatching.induce_connectedComponent, nontrivial_verts_of_degree_ne_zero, deleteVerts_inter_verts_set_right_eq, SimpleGraph.IsClique.even_iff_exists_isMatching, SimpleGraph.Copy.range_toSubgraph, IsMatching.exists_of_disjoint_sets_of_equiv, verts_top, SimpleGraph.IsTree.coe_subgraphOfAdj, coe_degree, SimpleGraph.nonempty_singletonSubgraph_verts, SimpleGraph.Walk.map_mapToSubgraph_eq_induce, coe_adj, SimpleGraph.ConnectedComponent.odd_matches_node_outside, Preconnected.degree_zero_iff, mem_verts_of_mem_edge, SimpleGraph.IsContained.exists_iso_subgraph, isAcyclic_coe_bot, support_subset_verts, SimpleGraph.Walk.mem_verts_toSubgraph, Adj.snd_mem, preconnected_iff, IsMatching.toEdge.surjective, SimpleGraph.Finsubgraph.coe_iInf, SimpleGraph.singletonSubgraph_verts, map_hom_top, Connected.exists_verts_eq_connectedComponentSupp, SimpleGraph.Finsubgraph.coe_bot, SimpleGraph.Reachable.coe_coeSubgraph, deleteEdges_coe_eq, SimpleGraph.IsTree.coe_singletonSubgraph, verts_monotone, verts_mono, coe_deleteEdges_le, map_verts, spanningCoeEquivCoeOfSpanning_apply_coe, verts_inf, SimpleGraph.nonempty_subgraphOfAdj_verts, Preconnected.coe, connected_iff_forall_exists_walk_subgraph, IsMatching.exists_of_universalVerts, SimpleGraph.Finsubgraph.coe_iSup, SimpleGraph.Walk.map_mapToSubgraph_hom, ne_bot_iff_nonempty_verts, Connected.nonempty, IsSpanning.card_verts, induce_verts, SimpleGraph.Walk.map_mapToSubgraph_eq_induce_id, hom_injective, SimpleGraph.Walk.end_mem_verts_toSubgraph, SimpleGraph.isIndepSet_induce, deleteVerts_verts, connected_iff', verts_iSup, SimpleGraph.Finsubgraph.coe_sup, SimpleGraph.Walk.verts_toSubgraph, verts_iInf, spanningCoeEquivCoeOfSpanning_symm_apply, SimpleGraph.Finsubgraph.coe_inf, SimpleGraph.Walk.IsCycle.exists_isCycle_snd_verts_eq, SimpleGraph.disjoint_image_val_universalVerts, IsSpanning.verts_eq_univ, SimpleGraph.subgraphOfAdj_verts, SimpleGraph.IsAcyclic.subgraph, SimpleGraph.Copy.toSubgraph_surjOn, edgeSet_coe, deleteEdges_verts, SimpleGraph.Finsubgraph.coe_himp, eq_bot_iff_verts_eq_empty, spanningCoe_coe, SimpleGraph.toSubgraph_verts, SimpleGraph.isNIndepSet_induce, IsInduced.induce_top_verts, deleteVerts_adj, SimpleGraph.singletonFinsubgraph_le_adj_left, induce_self_verts, SimpleGraph.Reachable.coe_toSubgraph, inclusion_apply_coe, isSpanning_iff, coeSubgraph_adj, ext_iff, connected_iff, verts_sSup, Adj.fst_mem, SimpleGraph.eq_singletonSubgraph_iff_verts_eq, SimpleGraph.Walk.start_mem_verts_toSubgraph, deleteVerts_inter_verts_left_eq, SimpleGraph.Reachable.coe_subgraphMap, Adj.coe, Connected.induce_verts, hom_apply, SimpleGraph.killCopies_def, SimpleGraph.Finsubgraph.coe_sInf, SimpleGraph.Finsubgraph.coe_compl, IsInduced.isIndContained, IsMatching.support_eq_verts, IsMatching.even_card, Preconnected.exists_adj_of_nontrivial, SimpleGraph.IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp, SimpleGraph.exists_isMatching_of_forall_ncard_le, inclusion.injective, verts_sInf, verts_bot, coe_hom, coe_deleteEdges_eq, restrict_adj, coe_isContained, SimpleGraph.singletonFinsubgraph_le_adj_right, Connected.coe, coe_bot
|