Adj 📖 | MathDef | 360 mathmath: adj_replaceVertex_iff_of_ne_right, TripartiteFromTriangles.Graph.in₀₂_iff', Iso.map_adj_iff, Matrix.IsAdjMatrix.toGraph_adj, Walk.adj_of_infix_support, Walk.adj_penultimate, IsTuranMaximal.not_adj_iff_part_eq, adj_replaceVertex_iff_of_ne, mem_incidenceSet, coe_induceHom, boxProd_adj_right, lapMatrix_toLinearMap₂', map_singletonSubgraph, Adj.symm, isVertexCover_preimage_iso, TopEdgeLabeling.labelGraph_adj, sInf_adj, Copy.coe_mk, two_mul_card_edgeFinset, Walk.map_copy, Walk.map_injective_of_injective, mem_support, adjMatrix_apply, homOfConnectedComponents_apply, Walk.exists_eq_cons_of_ne, adj_iff_exists_edge_coe, Coloring.mem_colorClass, exists_bijective_of_forall_ncard_le, Path.mapEmbedding_coe, dotProduct_mulVec_adjMatrix, Subgraph.IsInduced.adj, sum_adj, IsNClique.exists_not_adj_of_cliqueFree_succ, Iso.connectedComponentEquiv_symm_apply, Embedding.apply_mem_neighborSet_iff, adj_injective, Iso.reachable_iff, regularityReduced_adj, Embedding.sumInr_apply, EdgeLabeling.get_pullback, Subgraph.spanningHom_injective, Copy.topEmbedding_apply, Walk.IsCycle.map, card_le_chromaticNumber_iff_forall_surjective, TripartiteFromTriangles.Graph.in₀₁_iff', exists_adj_isEdgeReachable_two, Iso.sumComm_apply, TripartiteFromTriangles.Graph.in₂₁_iff', card_edgeFinset_map, adj_replaceVertex_iff_of_ne_left, Walk.exists_concat_eq_cons, Iso.sumBoxProdDistrib_apply, Iso.symm_apply_reachable, pathGraph_adj, Preconnected.exists_adj_of_nontrivial, cycleGraph_adj', Subgraph.comap_verts, hasseDualIso_apply, Embedding.map_adj_iff, induceUnivIso_apply, Iso.map_symm_apply, Copy.toHom_apply, completeMultipartiteGraph.topEmbedding_apply_fst, toTopEdgeLabeling_get, Hom.coe_id, edgeFinset_map, TripartiteFromTriangles.Graph.in₁₀_iff, Embedding.sumInl_apply, Walk.exists_adj_adj_not_adj_ne, Embedding.mapNeighborSet_apply_coe, Walk.adj_of_length_eq_one, exists_isTuranMaximal, deleteIncidenceSet_adj, mem_commonNeighbors, Walk.map_isCycle_iff_of_injective, TripartiteFromTriangles.graph_triple, eccent_le_one_iff, Embedding.map_mem_edgeSet_iff, Copy.injective, Subgraph.adj_sub, degree_pos_iff_exists_adj, Walk.map_mapToSubgraph_eq_induce, disjoint_edge, Walk.darts_map, Subgraph.coe_adj, adj_and_reachable_delete_edges_iff_exists_cycle, Walk.map_nil, Walk.cons_copy, Hom.map_adj, IsTuranMaximal.not_adj_trans, boxProd_adj_left, isBipartiteWith_neighborFinset, isIndepSet_iff, Walk.map_map, IsTuranMaximal.equivalence_not_adj, Iso.map_mem_edgeSet_iff, Walk.IsHamiltonian.map, isClique_pair, le_iff_adj, Subgraph.coeEmbeddingSpanningCoe_apply, IsPathGraph3Compl.not_adj_fst, completeEquipartiteGraph_adj, boxProdComm_symm_apply, Walk.induce_cons, isBridge_iff_adj_and_forall_walk_mem_edges, Walk.not_nil_iff, Hom.mapEdgeSet_coe, sup_adj, Iso.apply_mem_neighborSet_iff, fromEdgeSet_adj, Hom.map_mem_edgeSet, Subgraph.iInf_adj, cliqueFinset_map_of_equiv, map_adj, ruzsaSzemerediNumber_spec, IsPathGraph3Compl.not_adj_snd, Subgraph.sInf_adj, interedges_def, Subgraph.Adj.of_spanningCoe, ConnectedComponent.adj_spanningCoe_toSimpleGraph, TripartiteFromTriangles.Graph.in₀₂_iff, boxProdAssoc_apply, adj_edge, top_adj, Walk.map_isPath_iff_of_injective, Subgraph.coe_adj_sub, ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map, compl_adj, mem_neighborSet, Hom.mapDart_apply, Walk.IsSubwalk.map, Subgraph.adj_iff_of_neighborSet_equiv, Subgraph.edgeSet_map, ne_bot_iff_exists_adj, map_adj_apply, eccent_eq_one_iff, incMatrix_mul_transpose, le_chromaticNumber_iff_forall_surjective, Walk.isChain_adj_cons_support, iInf_adj, induceHom_injective, Subgraph.map_verts, Coloring.not_adj_of_mem_colorClass, Subgraph.spanningCoeEquivCoeOfSpanning_apply_coe, Embedding.coe_comp, ConnectedComponent.toSimpleGraph_hom_apply, Hom.comap_apply, extremalNumber_of_fintypeCard_eq, cliqueFinset_map, completeBipartiteGraph_adj, symm, isVertexCover_image_iso, Coloring.injective_comp_of_pairwise_adj, mk_mem_interedges_iff, Copy.injective', dist_eq_one_iff_adj, hasse_adj, unreduced_edges_subset, induceHomOfLE_apply, deleteEdges_adj, Walk.IsCycle.adj_toSubgraph_iff_of_isCycles, isBridge_iff, Hom.coe_comp, Subgraph.map_adj, comap_adj, isClique_insert_of_notMem, Walk.reverse_map, ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp, colorable_iff_exists_bdd_nat_coloring, isBridge_iff_adj_and_forall_cycle_notMem, Iso.mapNeighborSet_apply_coe, sSup_adj, cycleGraph_adj, Iso.comap_apply, Walk.map_mapToSubgraph_eq_induce_id, ne_top_iff_exists_not_adj, is3Clique_iff, Path.mapEmbedding_injective, isBipartiteWith_bipartiteBelow, isClique_iff_isChain_adj, Walk.length_map, Walk.adj_getVert_succ, Subgraph.hom_injective, triangle_counting', TripartiteFromTriangles.Graph.in₁₂_iff', edge_adj, TripartiteFromTriangles.Graph.in₂₀_iff', mem_interedges_iff, isBipartiteWith_neighborSet', Iso.connectedComponentEquiv_trans, mem_neighborFinset, Iso.boxProdSumDistrib_symm_apply, set_walk_length_succ_eq, edist_eq_two_iff, sdiff_adj, Reachable.map, reachable_iff_reflTransGen, adj_of_mem_walk_support, adj_symm, Hom.mapNeighborSet_coe, isClique_iff, Iso.boxProdSumDistrib_apply, induceHom_comp, bot_adj, measurable_iff_adj, Subgraph.Adj.adj_sub, Walk.IsPath.injOn_support_of_isPath_map, Iso.boxProdSumDistrib_toEquiv, ext_iff, eq_bot_iff_forall_not_adj, isClique_insert, Iso.degree_eq, turanGraph_adj, Walk.exists_cons_eq_concat, ConnectedComponent.map_mk, lt_extremalNumber_iff, exists_isExtremal_iff_exists, degree_eq_sum_if_adj, cycleGraph_one_adj, symm_adj, map_adj', Subgraph.spanningCoeEquivCoeOfSpanning_symm_apply, Walk.map_isTrail_iff_of_injective, loopless, mk'_mem_incidenceSet_left_iff, isBipartiteWith_neighborSet, isIndepSet_iff_isAntichain_adj, Walk.map_isTrail_of_injective, Embedding.map_apply, TripartiteFromTriangles.Graph.not_in₂₂, TripartiteFromTriangles.Graph.in₀₁_iff, between_adj, Coloring.color_classes_independent, adj_congr_of_sym2, disjoint_left, TripartiteFromTriangles.Graph.in₂₀_iff, boxProd_adj, iInf_adj_of_nonempty, boxProdAssoc_symm_apply, cliqueFreeOn_two, Subgraph.spanningHom_apply, Walk.adj_of_mem_edges, TripartiteFromTriangles.Graph.in₁₀_iff', completeMultipartiteGraph.topEmbedding_apply_snd, Iso.mapNeighborSet_symm_apply_coe, Walk.isChain_adj_support, mk'_apply_adj, Iso.sumAssoc_apply, Walk.map_cons, Embedding.comap_apply, TripartiteFromTriangles.Graph.in₁₂_iff, Iso.sumBoxProdDistrib_symm_apply, FirstOrder.Language.simpleGraphOfStructure_adj, lt_extremalNumber_iff_of_nonneg, Walk.map_isPath_of_injective, eq_top_iff_forall_ne_adj, Walk.toDeleteEdges_cons, irrefl, IsCycles.existsUnique_ne_adj, Walk.edgeSet_map, toSubgraph_adj, Subgraph.top_adj, not_isClique_iff, Coloring.surjOn_of_card_le_isClique, exists_isExtremal_free, Path.map_coe, Embedding.coe_completeGraph, Walk.IsHamiltonian.injective_of_isPath_map, is3Clique_triple_iff, sInf_adj_of_nonempty, triangle_removal, fromRel_adj, induceUnivIso_symm_apply_coe, Walk.map_append, ComponentCompl.exists_adj_boundary_pair, Subgraph.Adj.adj_sub', lineGraph_adj_iff_exists, measurable_adj, ConnectedComponent.toSimpleGraph_adj, neighborFinset_eq_filter, reachable_or_compl_adj, Walk.map_eq_of_eq, Embedding.mapEdgeSet_apply, Embedding.coe_toHom, Dart.adj, Subgraph.spanningCoe_adj, iSup_adj, Coloring.odd_length_iff_not_congr, circulantGraph_adj_translate, Subgraph.inclusion_apply_coe, hasseDualIso_symm_apply, isAcyclic_sup_fromEdgeSet_iff, Walk.support_map, boxProdRight_apply, isBridge_iff_adj_and_not_isEdgeConnected_two, cycleGraph_zero_adj, chromaticNumber_eq_iff_forall_surjective, Iso.mapEdgeSet_apply, mk'_mem_incidenceSet_iff, Walk.IsHamiltonianCycle.map, Walk.edges_map, induce_adj, Reachable.coe_subgraphMap, two_lt_edist_iff, Subgraph.Adj.coe, adj_le_reachable, Iso.connectedComponentEquiv_apply, Subgraph.hom_apply, Coloring.mem_colorClasses, adj_inj, Iso.coe_comp, Hom.injective_of_top_hom, mem_edgeSet, isBipartiteWith_bipartiteAbove, reachable_eq_reflTransGen, Path.map_injective, map_subgraphOfAdj, Hom.coe_ofLE, Walk.copy_cons, Walk.adj_snd, edge_le_iff, Partition.independent, not_adj_replaceVertex_same, adj_iff_exists_edge, adj_of_mem_incidenceSet, circulantGraph_adj, Walk.map_eq_nil_iff, EdgeLabeling.labelGraph_adj, TripartiteFromTriangles.Graph.not_in₀₀, Walk.exists_length_eq_one_iff, edist_eq_one_iff_adj, Subgraph.inclusion.injective, Iso.sumAssoc_symm_apply, mk'_mem_incidenceSet_right_iff, Coloring.even_length_iff_congr, TripartiteFromTriangles.Graph.not_in₁₁, Walk.getVert_map, TripartiteFromTriangles.Graph.in₂₁_iff, isBipartiteWith_neighborFinset', Iso.sumBoxProdDistrib_toEquiv, chromaticNumber_eq_card_iff_forall_surjective, Iso.mapEdgeSet_symm_apply, deleteUniversalVerts_adj, boxProdLeft_apply, IsPathGraph3Compl.adj, degree_eq_one_iff_existsUnique_adj, Iso.map_apply, adj_comm, boxProdComm_apply, Iso.comap_symm_apply, Walk.toSubgraph_map, Iso.sumComm_symm_apply, IsCycles.other_adj_of_adj, Subgraph.coe_hom, Subgraph.comap_adj, inf_adj, edist_le_one_iff_adj_or_eq, Hom.apply_mem_neighborSet, Copy.coe_toHom, Hom.ofLE_apply
|