Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 17:29 b6c96ef7

View on Github →

feat(combinatorics/simple_graph/clique): Clique-free graphs (#13552) ... and the finset of cliques of a finite graph.

Estimated changes

Modified src/combinatorics/simple_graph/clique.lean

added def simple_graph.clique_finset

added theorem simple_graph.clique_finset_eq_empty_iff

added theorem simple_graph.clique_finset_mono

added theorem simple_graph.clique_free.anti

added theorem simple_graph.clique_free.mono

added def simple_graph.clique_free

added theorem simple_graph.clique_free_bot

added theorem simple_graph.is_3_clique_iff

added theorem simple_graph.is_3_clique_triple_iff

added def simple_graph.is_clique

deleted structure simple_graph.is_clique

added theorem simple_graph.is_clique_bot_iff

modified theorem simple_graph.is_clique_iff

modified structure simple_graph.is_n_clique

added theorem simple_graph.is_n_clique_bot_iff

added theorem simple_graph.mem_clique_finset_iff

Modified src/data/set/pairwise.lean

added theorem set.pairwise_bot_iff