mathlib

58525685 - feat(combinatorics/simple_graph/{basic,subgraph,clique,coloring}): add induced graphs, characterization of cliques, and bounds for colorings (#14034)

feat(combinatorics/simple_graph/{basic,subgraph,clique,coloring}): add induced graphs, characterization of cliques, and bounds for colorings (#14034) This adds `simple_graph.map`, `simple_graph.comap`, and induced graphs and subgraphs. There are renamings: `simple_graph.subgraph.map` to `simple_graph.subgraph.inclusion`, `simple_graph.subgraph.map_top` to `simple_graph.subgraph.hom`, and `simple_graph.subgraph.map_spanning_top` to `simple_graph.subgraph.spanning_hom`. These changes originated to be able to express that a clique is a set of vertices whose induced subgraph is complete, which gives some clique-based bounds for chromatic numbers.