Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-10-22 19:51 3365b20c

View on Github →

feat(combinatorics/simple_graph): More clique lemmas (#19203) More lemmas about is_clique, is_n_clique, edge_set. Also define clique_free_on, a local version of clique_free.

Estimated changes

added theorem simple_graph.comap_id
deleted def simple_graph.hom.id
added theorem simple_graph.map_id
added theorem simple_graph.map_map
added theorem simple_graph.map_symm
modified theorem simple_graph.is_clique.mono
added theorem finset.exists_mem_ne
added theorem finset.preimage_map
added theorem iff.ne_left
added theorem iff.ne_right
added theorem relation.map_apply
added theorem relation.map_id_id
added theorem relation.map_map