Theorem SimpleGraph.not_cliqueFree_of_top_embedding

Modification history

2026-04-08 12:57

Mathlib/Combinatorics/SimpleGraph/Clique.lean

feat(Combinatorics/SimpleGraph/Clique): use `IsContained` instead of an explicit embedding from top (#35613) …

Deleted SimpleGraph.not_cliqueFree_of_top_embedding View on Github →

2023-02-27 13:48

Mathlib/Combinatorics/SimpleGraph/Clique.lean

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

Added SimpleGraph.not_cliqueFree_of_top_embedding View on Github →