Commit 2023-12-14 10:29 778aba64

View on Github →

feat: More clique lemmas (#8007) Forward port https://github.com/leanprover-community/mathlib/pull/19203

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

modified theorem SimpleGraph.Hom.coe_id

deleted theorem SimpleGraph.deleteEdges_eq

added theorem SimpleGraph.deleteEdges_eq_self

added theorem SimpleGraph.not_mem_neighborSet_self

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.CliqueFreeOn.anti

added theorem SimpleGraph.CliqueFreeOn.mono

added theorem SimpleGraph.CliqueFreeOn.of_succ

added theorem SimpleGraph.CliqueFreeOn.subset

added def SimpleGraph.CliqueFreeOn

added theorem SimpleGraph.IsClique.insert

modified theorem SimpleGraph.IsClique.mono

modified theorem SimpleGraph.IsClique.subset

added theorem SimpleGraph.IsNClique.insert

added theorem SimpleGraph.card_cliqueFinset_le

added theorem SimpleGraph.cliqueFinset_map

added theorem SimpleGraph.cliqueFinset_map_of_equiv

added theorem SimpleGraph.cliqueFreeOn_empty

added theorem SimpleGraph.cliqueFreeOn_of_card_lt

added theorem SimpleGraph.cliqueFreeOn_singleton

added theorem SimpleGraph.cliqueFreeOn_two

added theorem SimpleGraph.cliqueFreeOn_univ

added theorem SimpleGraph.cliqueFree_two

added theorem SimpleGraph.cliqueSet_bot

added theorem SimpleGraph.cliqueSet_map

added theorem SimpleGraph.cliqueSet_map_of_equiv

added theorem SimpleGraph.cliqueSet_one

added theorem SimpleGraph.cliqueSet_zero

added theorem SimpleGraph.isClique_empty

added theorem SimpleGraph.isClique_insert

added theorem SimpleGraph.isClique_insert_of_not_mem

added theorem SimpleGraph.isClique_pair

added theorem SimpleGraph.isClique_singleton

added theorem SimpleGraph.isNClique_empty

added theorem SimpleGraph.isNClique_one

added theorem SimpleGraph.isNClique_singleton

added theorem SimpleGraph.isNClique_zero

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.exists_mem_ne

Modified Mathlib/Data/Finset/Preimage.lean

added theorem Finset.preimage_map

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Logic/Relation.lean

added theorem Relation.map_apply