Commit 2024-06-22 19:24 78e28c0c

View on Github →

feat(SimpleGraph/Clique): maps of cliques (#12820) We add some API for cliques in maps of graphs.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.IsClique.of_subsingleton

added theorem SimpleGraph.cliqueFree_map_iff

added theorem SimpleGraph.isClique_map_finset_iff

added theorem SimpleGraph.isClique_map_finset_iff_of_nontrivial

added theorem SimpleGraph.isClique_map_iff

added theorem SimpleGraph.isClique_map_iff_of_nontrivial

added theorem SimpleGraph.isClique_map_image_iff

added theorem SimpleGraph.isNClique_map_iff