IsExtremal — Mathlib

English

If there exists a graph H with at least one edge, then there exists a graph G that is extremal with respect to H.Free.

Русский

Если существует граф $H$ с хотя бы одной реброй, то существует граф $G$, экстремальный по отношению к $H.Free$.

LaTeX

$$$\\exists G\\;\\exists \\text{ _ } : \\ DecidableRel G.Adj,\\; G.IsExtremal(H.Free)$$$

Lean4

/-- `G` is an extremal graph satisfying `p` if `G` has the maximum number of edges of any simple
graph satisfying `p`. -/
def IsExtremal (G : SimpleGraph V) [DecidableRel G.Adj] (p : SimpleGraph V → Prop) :=
  p G ∧ ∀ ⦃G' : SimpleGraph V⦄ [DecidableRel G'.Adj], p G' → #G'.edgeFinset ≤ #G.edgeFinset

Похожие утверждения