Commit 2026-04-08 12:57 93455d1b

View on Github →

feat(Combinatorics/SimpleGraph/Clique): use IsContained instead of an explicit embedding from top (#35613) This makes theorems require only a proof that a Copy exists rather than provide an explicit Embedding. Also tag monotonicity lemmas with @[gcongr], and add Copy.isContained / Embedding.isIndContained / Embedding.isContained / Iso.isContained'.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

modified theorem SimpleGraph.CliqueFree.comap

added theorem SimpleGraph.IsContained.not_cliqueFree

added theorem SimpleGraph.IsContained.not_cliqueFree_card

modified theorem SimpleGraph.cliqueFree_iff

deleted theorem SimpleGraph.not_cliqueFree_card_of_top_embedding

deleted theorem SimpleGraph.not_cliqueFree_iff

added theorem SimpleGraph.not_cliqueFree_iff_top_isContained

deleted theorem SimpleGraph.not_cliqueFree_of_top_embedding

Modified Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Copy.lean

Modified Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean