Theorems · Definition · combinatorics
SimpleGraph.IsTuranMaximal
{V : Type u_1} → [Fintype V] → (G : SimpleGraph V) → [DecidableRel G.Adj] → ℕ → PropAn r + 1-cliquefree graph is r-Turán-maximal if any other r + 1-cliquefree graph on
the same vertex set has the same or fewer number of edges.
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeDecidableRel
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Adjstatement and proof · cited by 1,346
- SimpleGraph.CliqueFreeproof · cited by 70
- SimpleGraph.IsExtremalproof · cited by 9
Cited by21
Results whose statement or proof uses this declaration.
- SimpleGraph.IsTuranMaximal.finpartitionstatement and proof · cited by 7
- SimpleGraph.IsTuranMaximal.not_adj_iff_part_eqstatement and proof · cited by 4
- SimpleGraph.isTuranMaximal_of_isostatement and proof · cited by 3
- SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraphstatement and proof · cited by 3
- SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraphstatement and proof · cited by 2
- SimpleGraph.exists_isTuranMaximalstatement · cited by 2
- SimpleGraph.isExtremal_top_free_iff_isTuranMaximalstatement · cited by 2
- SimpleGraph.isTuranMaximal_turanGraphstatement · cited by 1
- SimpleGraph.IsTuranMaximal.card_partsstatement and proof · cited by 1
- SimpleGraph.IsTuranMaximal.card_parts_lestatement and proof · cited by 1
- SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_cardstatement and proof · cited by 1
- SimpleGraph.IsTuranMaximal.degree_eq_of_not_adjstatement and proof · cited by 1