Theorems · Theorem · combinatorics
SimpleGraph.IsContained.not_cliqueFree
∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ}, (SimpleGraph.completeGraph (Fin n)).IsContained G → ¬G.CliqueFree n- Defined in
- Mathlib.Combinatorics.SimpleGraph.Clique
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finset.univproof · cited by 3,473
- SimpleGraphstatement and proof · cited by 3,072
- Fintype.cardproof · cited by 1,386
- Finset.mapproof · cited by 747
- Nonempty.someproof · cited by 340
- Fintype.card_finproof · cited by 270
- SimpleGraph.CliqueFreestatement and proof · cited by 70
- SimpleGraph.IsContainedstatement and proof · cited by 68
- SimpleGraph.IsNCliqueproof · cited by 64
- SimpleGraph.completeGraphstatement and proof · cited by 49
- SimpleGraph.Copy.toEmbeddingproof · cited by 9
- SimpleGraph.isNClique_map_copy_topproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- SimpleGraph.not_cliqueFree_iff_top_isContainedproof · cited by 7
- SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_infiniteproof · cited by 2
- SimpleGraph.not_cliqueFree_of_top_embeddingproof · cited by 0