Theorems · Definition · combinatorics

SimpleGraph.IsExtremal

{V : Type u_1} → [Fintype V] → (G : SimpleGraph V) → [DecidableRel G.Adj] → (SimpleGraph V → Prop) → Prop

G is an extremal graph satisfying p if G has the maximum number of edges of any simple graph, with fixed vertices, satisfying p.

Defined in

Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Cited by

9 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableRel