Commit 2022-06-26 23:29 f63d925e

View on Github →

feat(combinatorics/simple_graph/clique): The set of cliques (#14827) Define simple_graph.clique_set, the set analogue to simple_graph.clique_finset.

Estimated changes

Modified src/combinatorics/simple_graph/clique.lean

modified theorem simple_graph.clique_finset_mono

added def simple_graph.clique_set

added theorem simple_graph.clique_set_eq_empty_iff

added theorem simple_graph.clique_set_mono'

added theorem simple_graph.clique_set_mono

added theorem simple_graph.coe_clique_finset

modified theorem simple_graph.mem_clique_finset_iff

added theorem simple_graph.mem_clique_set_iff