Commit 2023-02-27 13:48 34352c15

View on Github →

feat: port Combinatorics.SimpleGraph.Clique (#2489)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.CliqueFree.anti

added theorem SimpleGraph.CliqueFree.mono

added def SimpleGraph.CliqueFree

added theorem SimpleGraph.IsClique.mono

added theorem SimpleGraph.IsClique.subset

added theorem SimpleGraph.IsNClique.mono

added theorem SimpleGraph.IsNClique.not_cliqueFree

added structure SimpleGraph.IsNClique

added def SimpleGraph.cliqueFinset

added theorem SimpleGraph.cliqueFinset_eq_empty_iff

added theorem SimpleGraph.cliqueFinset_mono

added theorem SimpleGraph.cliqueFree_bot

added theorem SimpleGraph.cliqueFree_iff

added theorem SimpleGraph.cliqueFree_of_card_lt

added def SimpleGraph.cliqueSet

added theorem SimpleGraph.cliqueSet_eq_empty_iff

added theorem SimpleGraph.cliqueSet_mono'

added theorem SimpleGraph.cliqueSet_mono

added theorem SimpleGraph.coe_cliqueFinset

added theorem SimpleGraph.is3Clique_iff

added theorem SimpleGraph.is3Clique_triple_iff

added theorem SimpleGraph.isClique_bot_iff

added theorem SimpleGraph.isClique_iff

added theorem SimpleGraph.isClique_iff_induce_eq

added theorem SimpleGraph.isNClique_bot_iff

added theorem SimpleGraph.isNClique_iff

added theorem SimpleGraph.mem_cliqueFinset_iff

added theorem SimpleGraph.mem_cliqueSet_iff

added theorem SimpleGraph.not_cliqueFree_card_of_top_embedding

added theorem SimpleGraph.not_cliqueFree_iff

added theorem SimpleGraph.not_cliqueFree_of_top_embedding