Theorems · Theorem · combinatorics
SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_card
∀ {n : ℕ} {ι : Type u_3} (V : ι → Type u_4) [inst : Fintype ι] (f : (i : ι) → V i),
n ≤ Fintype.card ι → ¬(SimpleGraph.completeMultipartiteGraph V).CliqueFree n- Defined in
- Mathlib.Combinatorics.SimpleGraph.Clique
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Equiv.symmproof · cited by 3,681
- Fintype.cardstatement and proof · cited by 1,386
- SimpleGraph.CliqueFreestatement and proof · cited by 70
- Fintype.equivFinproof · cited by 51
- IsEmpty.elim'proof · cited by 12
- SimpleGraph.completeMultipartiteGraphstatement and proof · cited by 11
- SimpleGraph.Iso.toCopyproof · cited by 7
- SimpleGraph.Embedding.toCopyproof · cited by 7
- SimpleGraph.Copy.compproof · cited by 5
- SimpleGraph.Iso.completeGraphproof · cited by 4
- SimpleGraph.completeMultipartiteGraph.topEmbeddingproof · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- SimpleGraph.completeMultipartiteGraph.colorable_of_cliqueFreeproof · cited by 1
- SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_enatCardproof · cited by 0
- SimpleGraph.completeMultipartiteGraph.chromaticNumberproof · cited by 0